Proof of Theorem pwfseqlem4a
Step | Hyp | Ref
| Expression |
1 | | isfinite 9118 |
. . 3
⊢ (𝑎 ∈ Fin ↔ 𝑎 ≺
ω) |
2 | | simpr 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → 𝑎 ∈ Fin) |
3 | | vex 3500 |
. . . . . . 7
⊢ 𝑠 ∈ V |
4 | | pwfseqlem4.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
5 | | pwfseqlem4.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ 𝐴) |
6 | | pwfseqlem4.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) |
7 | | pwfseqlem4.ps |
. . . . . . . 8
⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) |
8 | | pwfseqlem4.k |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–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 10084 |
. . . . . . 7
⊢ ((𝑎 ∈ Fin ∧ 𝑠 ∈ V) → (𝑎𝐹𝑠) = (𝐻‘(card‘𝑎))) |
12 | 2, 3, 11 | sylancl 588 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → (𝑎𝐹𝑠) = (𝐻‘(card‘𝑎))) |
13 | | f1of 6618 |
. . . . . . . . 9
⊢ (𝐻:ω–1-1-onto→𝑋 → 𝐻:ω⟶𝑋) |
14 | 6, 13 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ω⟶𝑋) |
15 | 14, 5 | fssd 6531 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ω⟶𝐴) |
16 | | ficardom 9393 |
. . . . . . 7
⊢ (𝑎 ∈ Fin →
(card‘𝑎) ∈
ω) |
17 | | ffvelrn 6852 |
. . . . . . 7
⊢ ((𝐻:ω⟶𝐴 ∧ (card‘𝑎) ∈ ω) → (𝐻‘(card‘𝑎)) ∈ 𝐴) |
18 | 15, 16, 17 | syl2an 597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → (𝐻‘(card‘𝑎)) ∈ 𝐴) |
19 | 12, 18 | eqeltrd 2916 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ Fin) → (𝑎𝐹𝑠) ∈ 𝐴) |
20 | 19 | ex 415 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ Fin → (𝑎𝐹𝑠) ∈ 𝐴)) |
21 | 20 | adantr 483 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎 ∈ Fin → (𝑎𝐹𝑠) ∈ 𝐴)) |
22 | 1, 21 | syl5bir 245 |
. 2
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎 ≺ ω → (𝑎𝐹𝑠) ∈ 𝐴)) |
23 | | omelon 9112 |
. . . . 5
⊢ ω
∈ On |
24 | | onenon 9381 |
. . . . 5
⊢ (ω
∈ On → ω ∈ dom card) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢ ω
∈ dom card |
26 | | simpr3 1192 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑠 We 𝑎) |
27 | 26 | 19.8ad 2180 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ∃𝑠 𝑠 We 𝑎) |
28 | | ween 9464 |
. . . . 5
⊢ (𝑎 ∈ dom card ↔
∃𝑠 𝑠 We 𝑎) |
29 | 27, 28 | sylibr 236 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑎 ∈ dom card) |
30 | | domtri2 9421 |
. . . 4
⊢ ((ω
∈ dom card ∧ 𝑎
∈ dom card) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω)) |
31 | 25, 29, 30 | sylancr 589 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω)) |
32 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑟(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) |
33 | | nfcv 2980 |
. . . . . . . . 9
⊢
Ⅎ𝑟𝑎 |
34 | | nfmpo2 7238 |
. . . . . . . . . 10
⊢
Ⅎ𝑟(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
35 | 10, 34 | nfcxfr 2978 |
. . . . . . . . 9
⊢
Ⅎ𝑟𝐹 |
36 | | nfcv 2980 |
. . . . . . . . 9
⊢
Ⅎ𝑟𝑠 |
37 | 33, 35, 36 | nfov 7189 |
. . . . . . . 8
⊢
Ⅎ𝑟(𝑎𝐹𝑠) |
38 | 37 | nfel1 2997 |
. . . . . . 7
⊢
Ⅎ𝑟(𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎) |
39 | 32, 38 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑟((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)) |
40 | | sseq1 3995 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝑟 ⊆ (𝑎 × 𝑎) ↔ 𝑠 ⊆ (𝑎 × 𝑎))) |
41 | | weeq1 5546 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝑟 We 𝑎 ↔ 𝑠 We 𝑎)) |
42 | 40, 41 | 3anbi23d 1435 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎))) |
43 | 42 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))) |
44 | 43 | anbi2d 630 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)))) |
45 | | oveq2 7167 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (𝑎𝐹𝑟) = (𝑎𝐹𝑠)) |
46 | 45 | eleq1d 2900 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → ((𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) ↔ (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))) |
47 | 44, 46 | imbi12d 347 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)))) |
48 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) |
49 | | nfcv 2980 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑎 |
50 | | nfmpo1 7237 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬
(𝐷‘𝑧) ∈ 𝑥}))) |
51 | 10, 50 | nfcxfr 2978 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
52 | | nfcv 2980 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑟 |
53 | 49, 51, 52 | nfov 7189 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑎𝐹𝑟) |
54 | 53 | nfel1 2997 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) |
55 | 48, 54 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) |
56 | | sseq1 3995 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴)) |
57 | | xpeq12 5583 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑎 ∧ 𝑥 = 𝑎) → (𝑥 × 𝑥) = (𝑎 × 𝑎)) |
58 | 57 | anidms 569 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (𝑥 × 𝑥) = (𝑎 × 𝑎)) |
59 | 58 | sseq2d 4002 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑎 × 𝑎))) |
60 | | weeq2 5547 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑎)) |
61 | 56, 59, 60 | 3anbi123d 1432 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎))) |
62 | | breq2 5073 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (ω ≼ 𝑥 ↔ ω ≼ 𝑎)) |
63 | 61, 62 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))) |
64 | 7, 63 | syl5bb 285 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝜓 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))) |
65 | 64 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))) |
66 | | oveq1 7166 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝑥𝐹𝑟) = (𝑎𝐹𝑟)) |
67 | | difeq2 4096 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑎)) |
68 | 66, 67 | eleq12d 2910 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → ((𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥) ↔ (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))) |
69 | 65, 68 | imbi12d 347 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)))) |
70 | 4, 5, 6, 7, 8, 9, 10 | pwfseqlem3 10085 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) |
71 | 55, 69, 70 | chvarfv 2241 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) |
72 | 39, 47, 71 | chvarfv 2241 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)) |
73 | 72 | eldifad 3951 |
. . . 4
⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) |
74 | 73 | expr 459 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 → (𝑎𝐹𝑠) ∈ 𝐴)) |
75 | 31, 74 | sylbird 262 |
. 2
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (¬ 𝑎 ≺ ω → (𝑎𝐹𝑠) ∈ 𝐴)) |
76 | 22, 75 | pm2.61d 181 |
1
⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) |