Proof of Theorem pwfseqlem4a
Step | Hyp | Ref
| Expression |
1 | | isfinite 8549 |
. . 3
⊢ (𝑎 ∈ Fin ↔ 𝑎 ≺
ω) |
2 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → 𝑎 ∈ Fin) |
3 | | vex 3203 |
. . . . . . 7
⊢ 𝑠 ∈ V |
4 | | pwfseqlem4.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
5 | | pwfseqlem4.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ 𝐴) |
6 | | pwfseqlem4.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) |
7 | | pwfseqlem4.ps |
. . . . . . . 8
⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) |
8 | | pwfseqlem4.k |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑𝑚
𝑛)–1-1→𝑥) |
9 | | pwfseqlem4.d |
. . . . . . . 8
⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) |
10 | | pwfseqlem4.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
11 | 4, 5, 6, 7, 8, 9, 10 | pwfseqlem2 9481 |
. . . . . . 7
⊢ ((𝑎 ∈ Fin ∧ 𝑠 ∈ V) → (𝑎𝐹𝑠) = (𝐻‘(card‘𝑎))) |
12 | 2, 3, 11 | sylancl 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → (𝑎𝐹𝑠) = (𝐻‘(card‘𝑎))) |
13 | | f1of 6137 |
. . . . . . . . 9
⊢ (𝐻:ω–1-1-onto→𝑋 → 𝐻:ω⟶𝑋) |
14 | 6, 13 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ω⟶𝑋) |
15 | 14, 5 | fssd 6057 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ω⟶𝐴) |
16 | | ficardom 8787 |
. . . . . . 7
⊢ (𝑎 ∈ Fin →
(card‘𝑎) ∈
ω) |
17 | | ffvelrn 6357 |
. . . . . . 7
⊢ ((𝐻:ω⟶𝐴 ∧ (card‘𝑎) ∈ ω) → (𝐻‘(card‘𝑎)) ∈ 𝐴) |
18 | 15, 16, 17 | syl2an 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → (𝐻‘(card‘𝑎)) ∈ 𝐴) |
19 | 12, 18 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → (𝑎𝐹𝑠) ∈ 𝐴) |
20 | 19 | ex 450 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ Fin → (𝑎𝐹𝑠) ∈ 𝐴)) |
21 | 20 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎 ∈ Fin → (𝑎𝐹𝑠) ∈ 𝐴)) |
22 | 1, 21 | syl5bir 233 |
. 2
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎 ≺ ω → (𝑎𝐹𝑠) ∈ 𝐴)) |
23 | | omelon 8543 |
. . . . 5
⊢ ω
∈ On |
24 | | onenon 8775 |
. . . . 5
⊢ (ω
∈ On → ω ∈ dom card) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢ ω
∈ dom card |
26 | | simpr3 1069 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑠 We 𝑎) |
27 | | 19.8a 2052 |
. . . . . 6
⊢ (𝑠 We 𝑎 → ∃𝑠 𝑠 We 𝑎) |
28 | 26, 27 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ∃𝑠 𝑠 We 𝑎) |
29 | | ween 8858 |
. . . . 5
⊢ (𝑎 ∈ dom card ↔
∃𝑠 𝑠 We 𝑎) |
30 | 28, 29 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑎 ∈ dom card) |
31 | | domtri2 8815 |
. . . 4
⊢ ((ω
∈ dom card ∧ 𝑎
∈ dom card) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω)) |
32 | 25, 30, 31 | sylancr 695 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω)) |
33 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑟(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) |
34 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑟𝑎 |
35 | | nfmpt22 6723 |
. . . . . . . . . 10
⊢
Ⅎ𝑟(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
36 | 10, 35 | nfcxfr 2762 |
. . . . . . . . 9
⊢
Ⅎ𝑟𝐹 |
37 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑟𝑠 |
38 | 34, 36, 37 | nfov 6676 |
. . . . . . . 8
⊢
Ⅎ𝑟(𝑎𝐹𝑠) |
39 | 38 | nfel1 2779 |
. . . . . . 7
⊢
Ⅎ𝑟(𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎) |
40 | 33, 39 | nfim 1825 |
. . . . . 6
⊢
Ⅎ𝑟((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)) |
41 | | sseq1 3626 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝑟 ⊆ (𝑎 × 𝑎) ↔ 𝑠 ⊆ (𝑎 × 𝑎))) |
42 | | weeq1 5102 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝑟 We 𝑎 ↔ 𝑠 We 𝑎)) |
43 | 41, 42 | 3anbi23d 1402 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎))) |
44 | 43 | anbi1d 741 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))) |
45 | 44 | anbi2d 740 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)))) |
46 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (𝑎𝐹𝑟) = (𝑎𝐹𝑠)) |
47 | 46 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → ((𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) ↔ (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))) |
48 | 45, 47 | imbi12d 334 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)))) |
49 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) |
50 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑎 |
51 | | nfmpt21 6722 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
52 | 10, 51 | nfcxfr 2762 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
53 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑟 |
54 | 50, 52, 53 | nfov 6676 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑎𝐹𝑟) |
55 | 54 | nfel1 2779 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) |
56 | 49, 55 | nfim 1825 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) |
57 | | sseq1 3626 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴)) |
58 | | xpeq12 5134 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑎 ∧ 𝑥 = 𝑎) → (𝑥 × 𝑥) = (𝑎 × 𝑎)) |
59 | 58 | anidms 677 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (𝑥 × 𝑥) = (𝑎 × 𝑎)) |
60 | 59 | sseq2d 3633 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑎 × 𝑎))) |
61 | | weeq2 5103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑎)) |
62 | 57, 60, 61 | 3anbi123d 1399 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎))) |
63 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (ω ≼ 𝑥 ↔ ω ≼ 𝑎)) |
64 | 62, 63 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))) |
65 | 7, 64 | syl5bb 272 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝜓 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))) |
66 | 65 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))) |
67 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝑥𝐹𝑟) = (𝑎𝐹𝑟)) |
68 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑎)) |
69 | 67, 68 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → ((𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥) ↔ (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))) |
70 | 66, 69 | imbi12d 334 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)))) |
71 | 4, 5, 6, 7, 8, 9, 10 | pwfseqlem3 9482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) |
72 | 56, 70, 71 | chvar 2262 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) |
73 | 40, 48, 72 | chvar 2262 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)) |
74 | 73 | eldifad 3586 |
. . . 4
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) |
75 | 74 | expr 643 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 → (𝑎𝐹𝑠) ∈ 𝐴)) |
76 | 32, 75 | sylbird 250 |
. 2
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (¬ 𝑎 ≺ ω → (𝑎𝐹𝑠) ∈ 𝐴)) |
77 | 22, 76 | pm2.61d 170 |
1
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) |