Step | Hyp | Ref
| Expression |
1 | | peano1 7085 |
. . . . . 6
⊢ ∅
∈ ω |
2 | | eqid 2622 |
. . . . . . . . . 10
⊢
{〈∅, 𝐶〉} = {〈∅, 𝐶〉} |
3 | | fsng 6404 |
. . . . . . . . . . 11
⊢ ((∅
∈ ω ∧ 𝐶
∈ 𝐴) →
({〈∅, 𝐶〉}:{∅}⟶{𝐶} ↔ {〈∅, 𝐶〉} = {〈∅, 𝐶〉})) |
4 | 1, 3 | mpan 706 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → ({〈∅, 𝐶〉}:{∅}⟶{𝐶} ↔ {〈∅, 𝐶〉} = {〈∅, 𝐶〉})) |
5 | 2, 4 | mpbiri 248 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉}:{∅}⟶{𝐶}) |
6 | | snssi 4339 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴) |
7 | 5, 6 | fssd 6057 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉}:{∅}⟶𝐴) |
8 | | suc0 5799 |
. . . . . . . . 9
⊢ suc
∅ = {∅} |
9 | 8 | feq2i 6037 |
. . . . . . . 8
⊢
({〈∅, 𝐶〉}:suc ∅⟶𝐴 ↔ {〈∅, 𝐶〉}:{∅}⟶𝐴) |
10 | 7, 9 | sylibr 224 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉}:suc ∅⟶𝐴) |
11 | | fvsng 6447 |
. . . . . . . 8
⊢ ((∅
∈ ω ∧ 𝐶
∈ 𝐴) →
({〈∅, 𝐶〉}‘∅) = 𝐶) |
12 | 1, 11 | mpan 706 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐴 → ({〈∅, 𝐶〉}‘∅) = 𝐶) |
13 | | ral0 4076 |
. . . . . . . 8
⊢
∀𝑘 ∈
∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)) |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐴 → ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘))) |
15 | 10, 12, 14 | 3jca 1242 |
. . . . . 6
⊢ (𝐶 ∈ 𝐴 → ({〈∅, 𝐶〉}:suc ∅⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) |
16 | | suceq 5790 |
. . . . . . . . 9
⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅) |
17 | 16 | feq2d 6031 |
. . . . . . . 8
⊢ (𝑚 = ∅ →
({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ↔ {〈∅, 𝐶〉}:suc ∅⟶𝐴)) |
18 | | raleq 3138 |
. . . . . . . 8
⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) |
19 | 17, 18 | 3anbi13d 1401 |
. . . . . . 7
⊢ (𝑚 = ∅ →
(({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘))) ↔ ({〈∅, 𝐶〉}:suc ∅⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘))))) |
20 | 19 | rspcev 3309 |
. . . . . 6
⊢ ((∅
∈ ω ∧ ({〈∅, 𝐶〉}:suc ∅⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) → ∃𝑚 ∈ ω ({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) |
21 | 1, 15, 20 | sylancr 695 |
. . . . 5
⊢ (𝐶 ∈ 𝐴 → ∃𝑚 ∈ ω ({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) |
22 | | axdc3lem4.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
23 | | axdc3lem4.2 |
. . . . . 6
⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} |
24 | | snex 4908 |
. . . . . 6
⊢
{〈∅, 𝐶〉} ∈ V |
25 | 22, 23, 24 | axdc3lem3 9274 |
. . . . 5
⊢
({〈∅, 𝐶〉} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) |
26 | 21, 25 | sylibr 224 |
. . . 4
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉} ∈ 𝑆) |
27 | | ne0i 3921 |
. . . 4
⊢
({〈∅, 𝐶〉} ∈ 𝑆 → 𝑆 ≠ ∅) |
28 | 26, 27 | syl 17 |
. . 3
⊢ (𝐶 ∈ 𝐴 → 𝑆 ≠ ∅) |
29 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆 |
30 | 22, 23 | axdc3lem 9272 |
. . . . . . . 8
⊢ 𝑆 ∈ V |
31 | 30 | elpw2 4828 |
. . . . . . 7
⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆) |
32 | 29, 31 | mpbir 221 |
. . . . . 6
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆 |
33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆) |
34 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
35 | 22, 23, 34 | axdc3lem3 9274 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) |
36 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → 𝑥:suc 𝑚⟶𝐴) |
37 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑚 ∈ V |
38 | 37 | sucid 5804 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑚 ∈ suc 𝑚 |
39 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑥‘𝑚) ∈ 𝐴) |
40 | 38, 39 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥‘𝑚) ∈ 𝐴) |
41 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥‘𝑚) ∈ 𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅})) |
42 | 40, 41 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅})) |
43 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅}) |
44 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹‘(𝑥‘𝑚)) ∈ V |
45 | 44 | elsn 4192 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) = ∅) |
46 | 45 | necon3bbii 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) ≠ ∅) |
47 | | n0 3931 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘(𝑥‘𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) |
48 | 46, 47 | bitri 264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) |
49 | 43, 48 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) |
50 | 42, 49 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) |
51 | | simp32 1098 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → 𝑥:suc 𝑚⟶𝐴) |
52 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) |
53 | | elelpwi 4171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) → 𝑧 ∈ 𝐴) |
54 | 53 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴)) |
55 | 42, 52, 54 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴)) |
56 | | peano2 7086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 ∈ ω → suc 𝑚 ∈
ω) |
57 | 56 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → suc 𝑚 ∈
ω) |
58 | 57 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω) |
59 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥:suc 𝑚⟶𝐴) |
60 | 34 | dmex 7099 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ dom 𝑥 ∈ V |
61 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ 𝑧 ∈ V |
62 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
{〈dom 𝑥, 𝑧〉} = {〈dom 𝑥, 𝑧〉} |
63 | | fsng 6404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((dom
𝑥 ∈ V ∧ 𝑧 ∈ V) → ({〈dom
𝑥, 𝑧〉}:{dom 𝑥}⟶{𝑧} ↔ {〈dom 𝑥, 𝑧〉} = {〈dom 𝑥, 𝑧〉})) |
64 | 62, 63 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((dom
𝑥 ∈ V ∧ 𝑧 ∈ V) → {〈dom
𝑥, 𝑧〉}:{dom 𝑥}⟶{𝑧}) |
65 | 60, 61, 64 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
{〈dom 𝑥, 𝑧〉}:{dom 𝑥}⟶{𝑧} |
66 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
67 | 66 | snssd 4340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {𝑧} ⊆ 𝐴) |
68 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(({〈dom 𝑥,
𝑧〉}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {〈dom 𝑥, 𝑧〉}:{dom 𝑥}⟶𝐴) |
69 | 65, 67, 68 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {〈dom 𝑥, 𝑧〉}:{dom 𝑥}⟶𝐴) |
70 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑥:suc 𝑚⟶𝐴 → dom 𝑥 = suc 𝑚) |
71 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω) |
72 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (dom
𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω)) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω)) |
74 | 71, 73 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω) |
75 | | nnord 7073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (dom
𝑥 ∈ ω → Ord
dom 𝑥) |
76 | | ordirr 5741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (Ord dom
𝑥 → ¬ dom 𝑥 ∈ dom 𝑥) |
77 | 74, 75, 76 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥) |
78 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (dom
𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚)) |
79 | 78 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚)) |
80 | 77, 79 | mtbid 314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚) |
81 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((suc
𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom
𝑥 ∈ suc 𝑚) |
82 | 80, 81 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅) |
83 | 70, 82 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅) |
84 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅) |
85 | | fun2 6067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑥:suc 𝑚⟶𝐴 ∧ {〈dom 𝑥, 𝑧〉}:{dom 𝑥}⟶𝐴) ∧ (suc 𝑚 ∩ {dom 𝑥}) = ∅) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴) |
86 | 59, 69, 84, 85 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴) |
87 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (dom
𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚}) |
88 | 87 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (dom
𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚})) |
89 | | df-suc 5729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ suc suc
𝑚 = (suc 𝑚 ∪ {suc 𝑚}) |
90 | 88, 89 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (dom
𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚) |
91 | 70, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑥:suc 𝑚⟶𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚) |
92 | 91 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚) |
93 | 92 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) |
94 | 86, 93 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴) |
95 | 94 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ 𝐴 → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) |
96 | 95 | adantrd 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) |
97 | 96 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴))) |
98 | 97 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴))) |
99 | 98 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴))) |
100 | 99 | 3imp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴) |
101 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑥:suc 𝑚⟶𝐴 → Fun 𝑥) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun 𝑥) |
103 | 60, 61 | funsn 5939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ Fun
{〈dom 𝑥, 𝑧〉} |
104 | 102, 103 | jctir 561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (Fun 𝑥 ∧ Fun {〈dom 𝑥, 𝑧〉})) |
105 | 61 | dmsnop 5609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ dom
{〈dom 𝑥, 𝑧〉} = {dom 𝑥} |
106 | 105 | ineq2i 3811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (dom
𝑥 ∩ dom {〈dom
𝑥, 𝑧〉}) = (dom 𝑥 ∩ {dom 𝑥}) |
107 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((dom
𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom
𝑥 ∈ dom 𝑥) |
108 | 77, 107 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅) |
109 | 106, 108 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {〈dom 𝑥, 𝑧〉}) = ∅) |
110 | 70, 109 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (dom 𝑥 ∩ dom {〈dom 𝑥, 𝑧〉}) = ∅) |
111 | | funun 5932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((Fun
𝑥 ∧ Fun {〈dom
𝑥, 𝑧〉}) ∧ (dom 𝑥 ∩ dom {〈dom 𝑥, 𝑧〉}) = ∅) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
112 | 104, 110,
111 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
113 | | ssun1 3776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
115 | | nnord 7073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑚 ∈ ω → Ord 𝑚) |
116 | | 0elsuc 7035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (Ord
𝑚 → ∅ ∈ suc
𝑚) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑚 ∈ ω → ∅
∈ suc 𝑚) |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ suc 𝑚) |
119 | 70 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑥:suc 𝑚⟶𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚)) |
120 | 119 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚)) |
121 | 118, 120 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ dom 𝑥) |
122 | | funssfv 6209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = (𝑥‘∅)) |
123 | 112, 114,
121, 122 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = (𝑥‘∅)) |
124 | 123 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶)) |
125 | 124 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶)) |
126 | 125 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶)) |
127 | 126 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶) |
128 | 127 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶) |
129 | 128 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶) |
130 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
Ⅎ𝑘∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) |
131 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
Ⅎ𝑘 𝑥:suc 𝑚⟶𝐴 |
132 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
Ⅎ𝑘 𝑚 ∈ ω |
133 | 130, 131,
132 | nf3an 1831 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑘(∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) |
134 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑘 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) |
135 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑘(𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) |
136 | 133, 134,
135 | nf3an 1831 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑘((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) |
137 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ suc 𝑚) |
138 | | elsuci 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑘 ∈ suc 𝑚 → (𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚)) |
139 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢
(∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑘 ∈ 𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) |
140 | 139 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝑘 ∈ 𝑚 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) |
141 | 140 | ad2ant2lr 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) |
142 | 141 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) |
143 | 112 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
144 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
145 | | ordsucelsuc 7022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ (Ord
𝑚 → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚)) |
146 | 115, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ (𝑚 ∈ ω → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚)) |
147 | 146 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → suc 𝑘 ∈ suc 𝑚) |
148 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ (dom
𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚)) |
149 | 148 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((suc
𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥) |
150 | 147, 70, 149 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom 𝑥) |
151 | | funssfv 6209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = (𝑥‘suc 𝑘)) |
152 | 143, 144,
150, 151 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = (𝑥‘suc 𝑘)) |
153 | 152 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = (𝑥‘suc 𝑘)) |
154 | 112 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
155 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
156 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (dom
𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚)) |
157 | 156 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥) |
158 | 70, 157 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥) |
159 | 158 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥) |
160 | | funssfv 6209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) |
161 | 154, 155,
159, 160 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) |
162 | 161 | 3adant1r 1319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) |
163 | 162 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) = (𝐹‘(𝑥‘𝑘))) |
164 | 153, 163 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) |
165 | 164 | 3adant2l 1320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) |
166 | 142, 165 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))) |
167 | 166 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
168 | 167 | 3expib 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) |
169 | 168 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑘 ∈ 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) |
170 | 112 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
171 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
{〈dom 𝑥, 𝑧〉} ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → {〈dom 𝑥, 𝑧〉} ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
173 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚) |
174 | 173 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚)) |
175 | 174 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘) |
176 | 60 | snid 4208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ dom 𝑥 ∈ {dom 𝑥} |
177 | 176, 105 | eleqtrri 2700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ dom 𝑥 ∈ dom {〈dom 𝑥, 𝑧〉} |
178 | 175, 177 | syl6eqelr 2710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) |
179 | 70, 178 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑘 = 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) |
180 | 179 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) |
181 | | funssfv 6209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ {〈dom 𝑥, 𝑧〉} ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = ({〈dom 𝑥, 𝑧〉}‘suc 𝑘)) |
182 | 170, 172,
180, 181 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = ({〈dom 𝑥, 𝑧〉}‘suc 𝑘)) |
183 | 175 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘) |
184 | 60, 61 | fvsn 6446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
({〈dom 𝑥, 𝑧〉}‘dom 𝑥) = 𝑧 |
185 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ (dom
𝑥 = suc 𝑘 → ({〈dom 𝑥, 𝑧〉}‘dom 𝑥) = ({〈dom 𝑥, 𝑧〉}‘suc 𝑘)) |
186 | 184, 185 | syl5reqr 2671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ (dom
𝑥 = suc 𝑘 → ({〈dom 𝑥, 𝑧〉}‘suc 𝑘) = 𝑧) |
187 | 183, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({〈dom 𝑥, 𝑧〉}‘suc 𝑘) = 𝑧) |
188 | 70, 187 | syl3an3 1361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({〈dom 𝑥, 𝑧〉}‘suc 𝑘) = 𝑧) |
189 | 182, 188 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = 𝑧) |
190 | 189 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = 𝑧) |
191 | 190 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = 𝑧) |
192 | 161 | 3adant1l 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) |
193 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ (𝑘 = 𝑚 → (𝑥‘𝑘) = (𝑥‘𝑚)) |
194 | 193 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (𝑥‘𝑘) = (𝑥‘𝑚)) |
195 | 194 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘𝑘) = (𝑥‘𝑚)) |
196 | 192, 195 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑚)) |
197 | 196 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) = (𝐹‘(𝑥‘𝑚))) |
198 | 191, 197 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))) |
199 | 198 | 3adant2l 1320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))) |
200 | 199 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
201 | 200 | 3expib 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) |
202 | 201 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) |
203 | 169, 202 | jaoi 394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) |
204 | 138, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) |
205 | 204 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) |
206 | 137, 205 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) |
207 | 206 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) |
208 | 207 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑘 ∈ suc 𝑚 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))))) |
209 | 208 | 3impd 1281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑘 ∈ suc 𝑚 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) |
210 | 209 | impd 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈ suc 𝑚 → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
211 | 210 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
212 | 211 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
213 | 136, 212 | ralrimi 2957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))) |
214 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚) |
215 | 214 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑝 = suc 𝑚 → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ↔ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) |
216 | | raleq 3138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑝 = suc 𝑚 → (∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
217 | 215, 216 | 3anbi13d 1401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑝 = suc 𝑚 → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))) ↔ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) |
218 | 217 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((suc
𝑚 ∈ ω ∧
((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
219 | 58, 100, 129, 213, 218 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
220 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
{〈dom 𝑥, 𝑧〉} ∈
V |
221 | 34, 220 | unex 6956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ V |
222 | 22, 23, 221 | axdc3lem3 9274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) |
223 | 219, 222 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆) |
224 | 223 | 3coml 1272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆) |
225 | 224 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆))) |
226 | 225 | expd 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → (𝑧 ∈ 𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)))) |
227 | 55, 226 | sylcom 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)))) |
228 | 227 | 3impd 1281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)) |
229 | 228 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚⟶𝐴 → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆))) |
230 | 229 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥:suc 𝑚⟶𝐴 → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆))) |
231 | 51, 230 | mpdi 45 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)) |
232 | 231 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆) |
233 | | resundir 5411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥)) |
234 | | frel 6050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥:suc 𝑚⟶𝐴 → Rel 𝑥) |
235 | | resdm 5441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (Rel
𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥) |
236 | 234, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥) |
237 | 236 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥) |
238 | 70, 74 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → dom 𝑥 ∈ ω) |
239 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (dom
𝑥 ∈ ω →
¬ dom 𝑥 ∈ dom
𝑥) |
240 | | incom 3805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ({dom
𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥}) |
241 | 240 | eqeq1i 2627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (({dom
𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅) |
242 | 60, 61 | fnsn 5946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
{〈dom 𝑥, 𝑧〉} Fn {dom 𝑥} |
243 | | fnresdisj 6001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
({〈dom 𝑥, 𝑧〉} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅)) |
244 | 242, 243 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (({dom
𝑥} ∩ dom 𝑥) = ∅ ↔ ({〈dom
𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) |
245 | 241, 244,
107 | 3bitr3ri 291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (¬
dom 𝑥 ∈ dom 𝑥 ↔ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) |
246 | 239, 245 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (dom
𝑥 ∈ ω →
({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) |
247 | 238, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) |
248 | 237, 247 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥)) = (𝑥 ∪ ∅)) |
249 | | un0 3967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∪ ∅) = 𝑥 |
250 | 248, 249 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥)) = 𝑥) |
251 | 233, 250 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) |
252 | 251 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) |
253 | 252 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) |
254 | 253 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) |
255 | 254 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) |
256 | 105 | uneq2i 3764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (dom
𝑥 ∪ dom {〈dom
𝑥, 𝑧〉}) = (dom 𝑥 ∪ {dom 𝑥}) |
257 | | dmun 5331 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ dom
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = (dom 𝑥 ∪ dom {〈dom 𝑥, 𝑧〉}) |
258 | | df-suc 5729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ suc dom
𝑥 = (dom 𝑥 ∪ {dom 𝑥}) |
259 | 256, 257,
258 | 3eqtr4i 2654 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 |
260 | 255, 259 | jctil 560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥)) |
261 | | dmeq 5324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → dom 𝑦 = dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) |
262 | 261 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥)) |
263 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥)) |
264 | 263 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥)) |
265 | 262, 264 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥))) |
266 | 265 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) |
267 | 232, 260,
266 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) |
268 | 267 | 3exp2 1285 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))) |
269 | 268 | exlimdv 1861 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))) |
270 | 269 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))) |
271 | 50, 270 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) |
272 | 271 | com3r 87 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) |
273 | 36, 272 | mpan2d 710 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) |
274 | 273 | com3r 87 |
. . . . . . . . . . . . . 14
⊢ ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) |
275 | 274 | 3expd 1284 |
. . . . . . . . . . . . 13
⊢ ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))) |
276 | 275 | com3r 87 |
. . . . . . . . . . . 12
⊢ (𝑥:suc 𝑚⟶𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))) |
277 | 276 | 3imp 1256 |
. . . . . . . . . . 11
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) |
278 | 277 | com12 32 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) |
279 | 278 | rexlimiv 3027 |
. . . . . . . . 9
⊢
(∃𝑚 ∈
ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))) |
280 | 35, 279 | sylbi 207 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))) |
281 | 280 | impcom 446 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) |
282 | | rabn0 3958 |
. . . . . . 7
⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) |
283 | 281, 282 | sylibr 224 |
. . . . . 6
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅) |
284 | 30 | rabex 4813 |
. . . . . . . 8
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V |
285 | 284 | elsn 4192 |
. . . . . . 7
⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅) |
286 | 285 | necon3bbii 2841 |
. . . . . 6
⊢ (¬
{𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅) |
287 | 283, 286 | sylibr 224 |
. . . . 5
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅}) |
288 | 33, 287 | eldifd 3585 |
. . . 4
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅})) |
289 | | axdc3lem4.3 |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)}) |
290 | 288, 289 | fmptd 6385 |
. . 3
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) |
291 | 30 | axdc2 9271 |
. . 3
⊢ ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) |
292 | 28, 290, 291 | syl2an 494 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) |
293 | 22, 23, 289 | axdc3lem2 9273 |
. 2
⊢
(∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |
294 | 292, 293 | syl 17 |
1
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |