Step | Hyp | Ref
| Expression |
1 | | peano1 7085 |
. . . 4
⊢ ∅
∈ ω |
2 | | opelxpi 5148 |
. . . 4
⊢ ((∅
∈ ω ∧ 𝐶
∈ 𝐴) →
〈∅, 𝐶〉
∈ (ω × 𝐴)) |
3 | 1, 2 | mpan 706 |
. . 3
⊢ (𝐶 ∈ 𝐴 → 〈∅, 𝐶〉 ∈ (ω × 𝐴)) |
4 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ω) |
5 | | fovrn 6804 |
. . . . . . . 8
⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) |
6 | | peano2 7086 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) |
7 | 6 | snssd 4340 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ω → {suc
𝑛} ⊆
ω) |
8 | | eldifi 3732 |
. . . . . . . . . 10
⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝑛𝐹𝑥) ∈ 𝒫 𝐴) |
9 | | axdc4lem.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈ V |
10 | 9 | elpw2 4828 |
. . . . . . . . . . 11
⊢ ((𝑛𝐹𝑥) ∈ 𝒫 𝐴 ↔ (𝑛𝐹𝑥) ⊆ 𝐴) |
11 | | xpss12 5225 |
. . . . . . . . . . 11
⊢ (({suc
𝑛} ⊆ ω ∧
(𝑛𝐹𝑥) ⊆ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴)) |
12 | 10, 11 | sylan2b 492 |
. . . . . . . . . 10
⊢ (({suc
𝑛} ⊆ ω ∧
(𝑛𝐹𝑥) ∈ 𝒫 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴)) |
13 | 7, 8, 12 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴)) |
14 | | snex 4908 |
. . . . . . . . . . 11
⊢ {suc
𝑛} ∈
V |
15 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑛𝐹𝑥) ∈ V |
16 | 14, 15 | xpex 6962 |
. . . . . . . . . 10
⊢ ({suc
𝑛} × (𝑛𝐹𝑥)) ∈ V |
17 | 16 | elpw 4164 |
. . . . . . . . 9
⊢ (({suc
𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴)) |
18 | 13, 17 | sylibr 224 |
. . . . . . . 8
⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴)) |
19 | 4, 5, 18 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴)) |
20 | | eldifn 3733 |
. . . . . . . 8
⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝑛𝐹𝑥) ∈ {∅}) |
21 | 15 | elsn 4192 |
. . . . . . . . . . 11
⊢ ((𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) = ∅) |
22 | 21 | necon3bbii 2841 |
. . . . . . . . . 10
⊢ (¬
(𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) ≠ ∅) |
23 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑛 ∈ V |
24 | 23 | sucex 7011 |
. . . . . . . . . . . 12
⊢ suc 𝑛 ∈ V |
25 | 24 | snnz 4309 |
. . . . . . . . . . 11
⊢ {suc
𝑛} ≠
∅ |
26 | | xpnz 5553 |
. . . . . . . . . . . 12
⊢ (({suc
𝑛} ≠ ∅ ∧
(𝑛𝐹𝑥) ≠ ∅) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅) |
27 | 26 | biimpi 206 |
. . . . . . . . . . 11
⊢ (({suc
𝑛} ≠ ∅ ∧
(𝑛𝐹𝑥) ≠ ∅) → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅) |
28 | 25, 27 | mpan 706 |
. . . . . . . . . 10
⊢ ((𝑛𝐹𝑥) ≠ ∅ → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅) |
29 | 22, 28 | sylbi 207 |
. . . . . . . . 9
⊢ (¬
(𝑛𝐹𝑥) ∈ {∅} → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅) |
30 | 16 | elsn 4192 |
. . . . . . . . . 10
⊢ (({suc
𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) = ∅) |
31 | 30 | necon3bbii 2841 |
. . . . . . . . 9
⊢ (¬
({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅) |
32 | 29, 31 | sylibr 224 |
. . . . . . . 8
⊢ (¬
(𝑛𝐹𝑥) ∈ {∅} → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅}) |
33 | 5, 20, 32 | 3syl 18 |
. . . . . . 7
⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅}) |
34 | 19, 33 | eldifd 3585 |
. . . . . 6
⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖
{∅})) |
35 | 34 | 3expib 1268 |
. . . . 5
⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) →
((𝑛 ∈ ω ∧
𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖
{∅}))) |
36 | 35 | ralrimivv 2970 |
. . . 4
⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) →
∀𝑛 ∈ ω
∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖
{∅})) |
37 | | axdc4lem.2 |
. . . . 5
⊢ 𝐺 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥))) |
38 | 37 | fmpt2 7237 |
. . . 4
⊢
(∀𝑛 ∈
ω ∀𝑥 ∈
𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}) ↔
𝐺:(ω × 𝐴)⟶(𝒫 (ω
× 𝐴) ∖
{∅})) |
39 | 36, 38 | sylib 208 |
. . 3
⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:(ω × 𝐴)⟶(𝒫 (ω
× 𝐴) ∖
{∅})) |
40 | | dcomex 9269 |
. . . . 5
⊢ ω
∈ V |
41 | 40, 9 | xpex 6962 |
. . . 4
⊢ (ω
× 𝐴) ∈
V |
42 | 41 | axdc3 9276 |
. . 3
⊢
((〈∅, 𝐶〉 ∈ (ω × 𝐴) ∧ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅})) →
∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) |
43 | 3, 39, 42 | syl2an 494 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) |
44 | | 2ndcof 7197 |
. . . . . . . . 9
⊢ (ℎ:ω⟶(ω ×
𝐴) → (2nd
∘ ℎ):ω⟶𝐴) |
45 | 44 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ (ℎ‘∅) = 〈∅,
𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ∘ ℎ):ω⟶𝐴) |
46 | 45 | adantl 482 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ):ω⟶𝐴) |
47 | | fex2 7121 |
. . . . . . . 8
⊢
(((2nd ∘ ℎ):ω⟶𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V) →
(2nd ∘ ℎ)
∈ V) |
48 | 40, 9, 47 | mp3an23 1416 |
. . . . . . 7
⊢
((2nd ∘ ℎ):ω⟶𝐴 → (2nd ∘ ℎ) ∈ V) |
49 | 46, 48 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ) ∈ V) |
50 | | fvco3 6275 |
. . . . . . . . . . 11
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ ∅ ∈
ω) → ((2nd ∘ ℎ)‘∅) = (2nd
‘(ℎ‘∅))) |
51 | 1, 50 | mpan2 707 |
. . . . . . . . . 10
⊢ (ℎ:ω⟶(ω ×
𝐴) → ((2nd
∘ ℎ)‘∅) =
(2nd ‘(ℎ‘∅))) |
52 | 51 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ (ℎ‘∅) = 〈∅,
𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) =
(2nd ‘(ℎ‘∅))) |
53 | | fveq2 6191 |
. . . . . . . . . 10
⊢ ((ℎ‘∅) = 〈∅,
𝐶〉 →
(2nd ‘(ℎ‘∅)) = (2nd
‘〈∅, 𝐶〉)) |
54 | 53 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ (ℎ‘∅) = 〈∅,
𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ‘(ℎ‘∅)) =
(2nd ‘〈∅, 𝐶〉)) |
55 | 52, 54 | eqtrd 2656 |
. . . . . . . 8
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ (ℎ‘∅) = 〈∅,
𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) =
(2nd ‘〈∅, 𝐶〉)) |
56 | | op2ndg 7181 |
. . . . . . . . 9
⊢ ((∅
∈ ω ∧ 𝐶
∈ 𝐴) →
(2nd ‘〈∅, 𝐶〉) = 𝐶) |
57 | 1, 56 | mpan 706 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → (2nd
‘〈∅, 𝐶〉) = 𝐶) |
58 | 55, 57 | sylan9eqr 2678 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ)‘∅) = 𝐶) |
59 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝐶 ∈ 𝐴 |
60 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 ℎ:ω⟶(ω ×
𝐴) |
61 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(ℎ‘∅) = 〈∅,
𝐶〉 |
62 | | nfra1 2941 |
. . . . . . . . . 10
⊢
Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) |
63 | 60, 61, 62 | nf3an 1831 |
. . . . . . . . 9
⊢
Ⅎ𝑘(ℎ:ω⟶(ω ×
𝐴) ∧ (ℎ‘∅) = 〈∅,
𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) |
64 | 59, 63 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) |
65 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅)) |
66 | | opeq1 4402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = ∅ → 〈𝑚, 𝑧〉 = 〈∅, 𝑧〉) |
67 | 65, 66 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = ∅ → ((ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ (ℎ‘∅) = 〈∅, 𝑧〉)) |
68 | 67 | exbidv 1850 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = ∅ → (∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ ∃𝑧(ℎ‘∅) = 〈∅, 𝑧〉)) |
69 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖)) |
70 | | opeq1 4402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑖 → 〈𝑚, 𝑧〉 = 〈𝑖, 𝑧〉) |
71 | 69, 70 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑖 → ((ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ (ℎ‘𝑖) = 〈𝑖, 𝑧〉)) |
72 | 71 | exbidv 1850 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑖 → (∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ ∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉)) |
73 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖)) |
74 | | opeq1 4402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = suc 𝑖 → 〈𝑚, 𝑧〉 = 〈suc 𝑖, 𝑧〉) |
75 | 73, 74 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ (ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉)) |
76 | 75 | exbidv 1850 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = suc 𝑖 → (∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ ∃𝑧(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉)) |
77 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝐶 → 〈∅, 𝑧〉 = 〈∅, 𝐶〉) |
78 | 77 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝐶 → ((ℎ‘∅) = 〈∅, 𝑧〉 ↔ (ℎ‘∅) = 〈∅,
𝐶〉)) |
79 | 78 | spcegv 3294 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ 𝐴 → ((ℎ‘∅) = 〈∅, 𝐶〉 → ∃𝑧(ℎ‘∅) = 〈∅, 𝑧〉)) |
80 | 79 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ‘∅) = 〈∅, 𝐶〉) → ∃𝑧(ℎ‘∅) = 〈∅, 𝑧〉) |
81 | 80 | 3ad2antr2 1227 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘∅) = 〈∅, 𝑧〉) |
82 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℎ‘𝑖) = 〈𝑖, 𝑧〉 → (𝐺‘(ℎ‘𝑖)) = (𝐺‘〈𝑖, 𝑧〉)) |
83 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖𝐺𝑧) = (𝐺‘〈𝑖, 𝑧〉) |
84 | 82, 83 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℎ‘𝑖) = 〈𝑖, 𝑧〉 → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧)) |
85 | 84 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = 〈𝑖, 𝑧〉) → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧)) |
86 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = 〈𝑖, 𝑧〉) → 𝑖 ∈ ω) |
87 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ (ω × 𝐴)) |
88 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ((ℎ‘𝑖) ∈ (ω × 𝐴) ↔ 〈𝑖, 𝑧〉 ∈ (ω × 𝐴))) |
89 | | opelxp2 5151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑖, 𝑧〉 ∈ (ω ×
𝐴) → 𝑧 ∈ 𝐴) |
90 | 88, 89 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ((ℎ‘𝑖) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)) |
91 | 87, 90 | mpan9 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = 〈𝑖, 𝑧〉) → 𝑧 ∈ 𝐴) |
92 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑖 → suc 𝑛 = suc 𝑖) |
93 | 92 | sneqd 4189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑖 → {suc 𝑛} = {suc 𝑖}) |
94 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑖 → (𝑛𝐹𝑥) = (𝑖𝐹𝑥)) |
95 | 93, 94 | xpeq12d 5140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑖 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑥))) |
96 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 𝑧 → (𝑖𝐹𝑥) = (𝑖𝐹𝑧)) |
97 | 96 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = 𝑧 → ({suc 𝑖} × (𝑖𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑧))) |
98 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {suc
𝑖} ∈
V |
99 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖𝐹𝑧) ∈ V |
100 | 98, 99 | xpex 6962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({suc
𝑖} × (𝑖𝐹𝑧)) ∈ V |
101 | 95, 97, 37, 100 | ovmpt2 6796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧))) |
102 | 86, 91, 101 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = 〈𝑖, 𝑧〉) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧))) |
103 | 85, 102 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = 〈𝑖, 𝑧〉) → (𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧))) |
104 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖) |
105 | 104 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖)) |
106 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖)) |
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖))) |
108 | 105, 107 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))) |
109 | 108 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ ω →
(∀𝑘 ∈ ω
(ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))) |
110 | 109 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = 〈𝑖, 𝑧〉) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))) |
111 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)))) |
112 | | elxp 5131 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑖) = 〈𝑠, 𝑡〉 ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧)))) |
113 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑠 ∈ {suc 𝑖} ↔ 𝑠 = suc 𝑖) |
114 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑠 = suc 𝑖 → 〈𝑠, 𝑡〉 = 〈suc 𝑖, 𝑡〉) |
115 | 113, 114 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑠 ∈ {suc 𝑖} → 〈𝑠, 𝑡〉 = 〈suc 𝑖, 𝑡〉) |
116 | 115 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑠 ∈ {suc 𝑖} → ((ℎ‘suc 𝑖) = 〈𝑠, 𝑡〉 ↔ (ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉)) |
117 | 116 | biimpac 503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((ℎ‘suc 𝑖) = 〈𝑠, 𝑡〉 ∧ 𝑠 ∈ {suc 𝑖}) → (ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉) |
118 | 117 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((ℎ‘suc 𝑖) = 〈𝑠, 𝑡〉 ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → (ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉) |
119 | 118 | eximi 1762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑡((ℎ‘suc 𝑖) = 〈𝑠, 𝑡〉 ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉) |
120 | 119 | exlimiv 1858 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑠∃𝑡((ℎ‘suc 𝑖) = 〈𝑠, 𝑡〉 ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉) |
121 | 112, 120 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉) |
122 | 111, 121 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉)) |
123 | 103, 110,
122 | sylsyld 61 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = 〈𝑖, 𝑧〉) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉)) |
124 | 123 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉))) |
125 | 124 | exlimiv 1858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉))) |
126 | 125 | com3l 89 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉))) |
127 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → 〈suc 𝑖, 𝑡〉 = 〈suc 𝑖, 𝑧〉) |
128 | 127 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ((ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉 ↔ (ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉)) |
129 | 128 | cbvexv 2275 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑡(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑡〉 ↔ ∃𝑧(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉) |
130 | 126, 129 | syl8ib 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ∃𝑧(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉))) |
131 | 130 | impancom 456 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ∃𝑧(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉))) |
132 | 131 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ (ℎ‘∅) = 〈∅,
𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ∃𝑧(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉))) |
133 | 132 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ∃𝑧(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉))) |
134 | 133 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (∃𝑧(ℎ‘𝑖) = 〈𝑖, 𝑧〉 → ∃𝑧(ℎ‘suc 𝑖) = 〈suc 𝑖, 𝑧〉))) |
135 | 68, 72, 76, 81, 134 | finds2 7094 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉)) |
136 | 135 | com12 32 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ ω → ∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉)) |
137 | 136 | ralrimiv 2965 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉) |
138 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑘 → (ℎ‘𝑚) = (ℎ‘𝑘)) |
139 | | opeq1 4402 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑘 → 〈𝑚, 𝑧〉 = 〈𝑘, 𝑧〉) |
140 | 138, 139 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑘 → ((ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ (ℎ‘𝑘) = 〈𝑘, 𝑧〉)) |
141 | 140 | exbidv 1850 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → (∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉 ↔ ∃𝑧(ℎ‘𝑘) = 〈𝑘, 𝑧〉)) |
142 | 141 | rspccv 3306 |
. . . . . . . . . . . 12
⊢
(∀𝑚 ∈
ω ∃𝑧(ℎ‘𝑚) = 〈𝑚, 𝑧〉 → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = 〈𝑘, 𝑧〉)) |
143 | 137, 142 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = 〈𝑘, 𝑧〉)) |
144 | 143 | 3impia 1261 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ∃𝑧(ℎ‘𝑘) = 〈𝑘, 𝑧〉) |
145 | | simp21 1094 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ℎ:ω⟶(ω × 𝐴)) |
146 | | simp3 1063 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ω) |
147 | | rspa 2930 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) |
148 | 147 | 3ad2antl3 1225 |
. . . . . . . . . . 11
⊢ (((ℎ:ω⟶(ω ×
𝐴) ∧ (ℎ‘∅) = 〈∅,
𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) |
149 | 148 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) |
150 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = 〈𝑘, 𝑧〉) |
151 | 150 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = (𝐺‘〈𝑘, 𝑧〉)) |
152 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω) |
153 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑘 ∈ ω) → (ℎ‘𝑘) ∈ (ω × 𝐴)) |
154 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ‘𝑘) ∈ (ω × 𝐴) ↔ 〈𝑘, 𝑧〉 ∈ (ω × 𝐴))) |
155 | | opelxp2 5151 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑘, 𝑧〉 ∈ (ω ×
𝐴) → 𝑧 ∈ 𝐴) |
156 | 154, 155 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ‘𝑘) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)) |
157 | 153, 156 | syl5 34 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → 𝑧 ∈ 𝐴)) |
158 | 157 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑧 ∈ 𝐴) |
159 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘𝐺𝑧) = (𝐺‘〈𝑘, 𝑧〉) |
160 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘) |
161 | 160 | sneqd 4189 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → {suc 𝑛} = {suc 𝑘}) |
162 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → (𝑛𝐹𝑥) = (𝑘𝐹𝑥)) |
163 | 161, 162 | xpeq12d 5140 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑥))) |
164 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝑘𝐹𝑥) = (𝑘𝐹𝑧)) |
165 | 164 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → ({suc 𝑘} × (𝑘𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑧))) |
166 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {suc
𝑘} ∈
V |
167 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘𝐹𝑧) ∈ V |
168 | 166, 167 | xpex 6962 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({suc
𝑘} × (𝑘𝐹𝑧)) ∈ V |
169 | 163, 165,
37, 168 | ovmpt2 6796 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑘𝐺𝑧) = ({suc 𝑘} × (𝑘𝐹𝑧))) |
170 | 159, 169 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝐺‘〈𝑘, 𝑧〉) = ({suc 𝑘} × (𝑘𝐹𝑧))) |
171 | 152, 158,
170 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘〈𝑘, 𝑧〉) = ({suc 𝑘} × (𝑘𝐹𝑧))) |
172 | 151, 171 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = ({suc 𝑘} × (𝑘𝐹𝑧))) |
173 | 172 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)))) |
174 | | elxp 5131 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)))) |
175 | | peano2 7086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) |
176 | | fvco3 6275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ suc 𝑘 ∈ ω) →
((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘))) |
177 | 175, 176 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘suc 𝑘) = (2nd
‘(ℎ‘suc 𝑘))) |
178 | 177 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd
∘ ℎ)‘suc 𝑘) = (2nd
‘(ℎ‘suc 𝑘))) |
179 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉) |
180 | 179 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd
‘(ℎ‘suc 𝑘)) = (2nd
‘〈𝑠, 𝑡〉)) |
181 | 178, 180 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd
∘ ℎ)‘suc 𝑘) = (2nd
‘〈𝑠, 𝑡〉)) |
182 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑠 ∈ V |
183 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑡 ∈ V |
184 | 182, 183 | op2nd 7177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2nd ‘〈𝑠, 𝑡〉) = 𝑡 |
185 | 181, 184 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd
∘ ℎ)‘suc 𝑘) = 𝑡) |
186 | | fvco3 6275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℎ:ω⟶(ω ×
𝐴) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘𝑘) = (2nd
‘(ℎ‘𝑘))) |
187 | 186 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd
∘ ℎ)‘𝑘) = (2nd
‘(ℎ‘𝑘))) |
188 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = 〈𝑘, 𝑧〉) |
189 | 188 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd
‘(ℎ‘𝑘)) = (2nd
‘〈𝑘, 𝑧〉)) |
190 | 187, 189 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd
∘ ℎ)‘𝑘) = (2nd
‘〈𝑘, 𝑧〉)) |
191 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑘 ∈ V |
192 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑧 ∈ V |
193 | 191, 192 | op2nd 7177 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(2nd ‘〈𝑘, 𝑧〉) = 𝑧 |
194 | 190, 193 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd
∘ ℎ)‘𝑘) = 𝑧) |
195 | 194 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) = (𝑘𝐹𝑧)) |
196 | 185, 195 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) ↔ 𝑡 ∈ (𝑘𝐹𝑧))) |
197 | 196 | biimprcd 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (ℎ‘𝑘) = 〈𝑘, 𝑧〉) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))) |
198 | 197 | exp4c 636 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 → ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))) |
199 | 198 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)) → ((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 → ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))) |
200 | 199 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
⊢ (((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))) |
201 | 200 | exlimivv 1860 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑠∃𝑡((ℎ‘suc 𝑘) = 〈𝑠, 𝑡〉 ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))) |
202 | 174, 201 | sylbi 207 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))) |
203 | 202 | com3l 89 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))) |
204 | 203 | imp 445 |
. . . . . . . . . . . . . 14
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))) |
205 | 173, 204 | sylbid 230 |
. . . . . . . . . . . . 13
⊢ (((ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))) |
206 | 205 | ex 450 |
. . . . . . . . . . . 12
⊢ ((ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))) |
207 | 206 | exlimiv 1858 |
. . . . . . . . . . 11
⊢
(∃𝑧(ℎ‘𝑘) = 〈𝑘, 𝑧〉 → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))) |
208 | 207 | 3imp 1256 |
. . . . . . . . . 10
⊢
((∃𝑧(ℎ‘𝑘) = 〈𝑘, 𝑧〉 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) ∧ (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))) |
209 | 144, 145,
146, 149, 208 | syl121anc 1331 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))) |
210 | 209 | 3expia 1267 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))) |
211 | 64, 210 | ralrimi 2957 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑘 ∈ ω ((2nd ∘
ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))) |
212 | 46, 58, 211 | 3jca 1242 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘
ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))) |
213 | | feq1 6026 |
. . . . . . . 8
⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔:ω⟶𝐴 ↔ (2nd ∘ ℎ):ω⟶𝐴)) |
214 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘∅) = ((2nd ∘
ℎ)‘∅)) |
215 | 214 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘∅) = 𝐶 ↔ ((2nd ∘ ℎ)‘∅) = 𝐶)) |
216 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘suc 𝑘) = ((2nd ∘ ℎ)‘suc 𝑘)) |
217 | | fveq1 6190 |
. . . . . . . . . . 11
⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘𝑘) = ((2nd ∘ ℎ)‘𝑘)) |
218 | 217 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑔 = (2nd ∘ ℎ) → (𝑘𝐹(𝑔‘𝑘)) = (𝑘𝐹((2nd ∘ ℎ)‘𝑘))) |
219 | 216, 218 | eleq12d 2695 |
. . . . . . . . 9
⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))) |
220 | 219 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑔 = (2nd ∘ ℎ) → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω ((2nd ∘
ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))) |
221 | 213, 215,
220 | 3anbi123d 1399 |
. . . . . . 7
⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))) ↔ ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘
ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))) |
222 | 221 | spcegv 3294 |
. . . . . 6
⊢
((2nd ∘ ℎ) ∈ V → (((2nd ∘
ℎ):ω⟶𝐴 ∧ ((2nd ∘
ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd
∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))) |
223 | 49, 212, 222 | sylc 65 |
. . . . 5
⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))) |
224 | 223 | ex 450 |
. . . 4
⊢ (𝐶 ∈ 𝐴 → ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))) |
225 | 224 | exlimdv 1861 |
. . 3
⊢ (𝐶 ∈ 𝐴 → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))) |
226 | 225 | adantr 481 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = 〈∅, 𝐶〉 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))) |
227 | 43, 226 | mpd 15 |
1
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))) |