| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | peano1 7911 | . . . . . 6
⊢ ∅
∈ ω | 
| 2 |  | eqid 2736 | . . . . . . . . . 10
⊢
{〈∅, 𝐶〉} = {〈∅, 𝐶〉} | 
| 3 |  | fsng 7156 | . . . . . . . . . . 11
⊢ ((∅
∈ ω ∧ 𝐶
∈ 𝐴) →
({〈∅, 𝐶〉}:{∅}⟶{𝐶} ↔ {〈∅, 𝐶〉} = {〈∅, 𝐶〉})) | 
| 4 | 1, 3 | mpan 690 | . . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → ({〈∅, 𝐶〉}:{∅}⟶{𝐶} ↔ {〈∅, 𝐶〉} = {〈∅, 𝐶〉})) | 
| 5 | 2, 4 | mpbiri 258 | . . . . . . . . 9
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉}:{∅}⟶{𝐶}) | 
| 6 |  | snssi 4807 | . . . . . . . . 9
⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴) | 
| 7 | 5, 6 | fssd 6752 | . . . . . . . 8
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉}:{∅}⟶𝐴) | 
| 8 |  | suc0 6458 | . . . . . . . . 9
⊢ suc
∅ = {∅} | 
| 9 | 8 | feq2i 6727 | . . . . . . . 8
⊢
({〈∅, 𝐶〉}:suc ∅⟶𝐴 ↔ {〈∅, 𝐶〉}:{∅}⟶𝐴) | 
| 10 | 7, 9 | sylibr 234 | . . . . . . 7
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉}:suc ∅⟶𝐴) | 
| 11 |  | fvsng 7201 | . . . . . . . 8
⊢ ((∅
∈ ω ∧ 𝐶
∈ 𝐴) →
({〈∅, 𝐶〉}‘∅) = 𝐶) | 
| 12 | 1, 11 | mpan 690 | . . . . . . 7
⊢ (𝐶 ∈ 𝐴 → ({〈∅, 𝐶〉}‘∅) = 𝐶) | 
| 13 |  | ral0 4512 | . . . . . . . 8
⊢
∀𝑘 ∈
∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)) | 
| 14 | 13 | a1i 11 | . . . . . . 7
⊢ (𝐶 ∈ 𝐴 → ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘))) | 
| 15 | 10, 12, 14 | 3jca 1128 | . . . . . 6
⊢ (𝐶 ∈ 𝐴 → ({〈∅, 𝐶〉}:suc ∅⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) | 
| 16 |  | suceq 6449 | . . . . . . . . 9
⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅) | 
| 17 | 16 | feq2d 6721 | . . . . . . . 8
⊢ (𝑚 = ∅ →
({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ↔ {〈∅, 𝐶〉}:suc ∅⟶𝐴)) | 
| 18 |  | raleq 3322 | . . . . . . . 8
⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) | 
| 19 | 17, 18 | 3anbi13d 1439 | . . . . . . 7
⊢ (𝑚 = ∅ →
(({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘))) ↔ ({〈∅, 𝐶〉}:suc ∅⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘))))) | 
| 20 | 19 | rspcev 3621 | . . . . . 6
⊢ ((∅
∈ ω ∧ ({〈∅, 𝐶〉}:suc ∅⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) → ∃𝑚 ∈ ω ({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) | 
| 21 | 1, 15, 20 | sylancr 587 | . . . . 5
⊢ (𝐶 ∈ 𝐴 → ∃𝑚 ∈ ω ({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) | 
| 22 |  | axdc3lem4.1 | . . . . . 6
⊢ 𝐴 ∈ V | 
| 23 |  | axdc3lem4.2 | . . . . . 6
⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} | 
| 24 |  | snex 5435 | . . . . . 6
⊢
{〈∅, 𝐶〉} ∈ V | 
| 25 | 22, 23, 24 | axdc3lem3 10493 | . . . . 5
⊢
({〈∅, 𝐶〉} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({〈∅, 𝐶〉}:suc 𝑚⟶𝐴 ∧ ({〈∅, 𝐶〉}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({〈∅, 𝐶〉}‘suc 𝑘) ∈ (𝐹‘({〈∅, 𝐶〉}‘𝑘)))) | 
| 26 | 21, 25 | sylibr 234 | . . . 4
⊢ (𝐶 ∈ 𝐴 → {〈∅, 𝐶〉} ∈ 𝑆) | 
| 27 | 26 | ne0d 4341 | . . 3
⊢ (𝐶 ∈ 𝐴 → 𝑆 ≠ ∅) | 
| 28 | 22, 23 | axdc3lem 10491 | . . . . . . 7
⊢ 𝑆 ∈ V | 
| 29 |  | ssrab2 4079 | . . . . . . 7
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆 | 
| 30 | 28, 29 | elpwi2 5334 | . . . . . 6
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆 | 
| 31 | 30 | a1i 11 | . . . . 5
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆) | 
| 32 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑥 ∈ V | 
| 33 | 22, 23, 32 | axdc3lem3 10493 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) | 
| 34 |  | simp2 1137 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → 𝑥:suc 𝑚⟶𝐴) | 
| 35 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑚 ∈ V | 
| 36 | 35 | sucid 6465 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑚 ∈ suc 𝑚 | 
| 37 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑥‘𝑚) ∈ 𝐴) | 
| 38 | 36, 37 | mpan2 691 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥‘𝑚) ∈ 𝐴) | 
| 39 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥‘𝑚) ∈ 𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅})) | 
| 40 | 38, 39 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅})) | 
| 41 |  | eldifn 4131 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅}) | 
| 42 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹‘(𝑥‘𝑚)) ∈ V | 
| 43 | 42 | elsn 4640 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) = ∅) | 
| 44 | 43 | necon3bbii 2987 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) ≠ ∅) | 
| 45 |  | n0 4352 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘(𝑥‘𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) | 
| 46 | 44, 45 | bitri 275 | . . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) | 
| 47 | 41, 46 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) | 
| 48 | 40, 47 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) | 
| 49 |  | simp32 1210 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → 𝑥:suc 𝑚⟶𝐴) | 
| 50 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) | 
| 51 |  | elelpwi 4609 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) → 𝑧 ∈ 𝐴) | 
| 52 | 51 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴)) | 
| 53 | 40, 50, 52 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴)) | 
| 54 |  | peano2 7913 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 ∈ ω → suc 𝑚 ∈
ω) | 
| 55 | 54 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → suc 𝑚 ∈
ω) | 
| 56 | 55 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω) | 
| 57 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥:suc 𝑚⟶𝐴) | 
| 58 | 32 | dmex 7932 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ dom 𝑥 ∈ V | 
| 59 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ 𝑧 ∈ V | 
| 60 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
{〈dom 𝑥, 𝑧〉} = {〈dom 𝑥, 𝑧〉} | 
| 61 |  | fsng 7156 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((dom
𝑥 ∈ V ∧ 𝑧 ∈ V) → ({〈dom
𝑥, 𝑧〉}:{dom 𝑥}⟶{𝑧} ↔ {〈dom 𝑥, 𝑧〉} = {〈dom 𝑥, 𝑧〉})) | 
| 62 | 60, 61 | mpbiri 258 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((dom
𝑥 ∈ V ∧ 𝑧 ∈ V) → {〈dom
𝑥, 𝑧〉}:{dom 𝑥}⟶{𝑧}) | 
| 63 | 58, 59, 62 | mp2an 692 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
{〈dom 𝑥, 𝑧〉}:{dom 𝑥}⟶{𝑧} | 
| 64 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) | 
| 65 | 64 | snssd 4808 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {𝑧} ⊆ 𝐴) | 
| 66 |  | fss 6751 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(({〈dom 𝑥,
𝑧〉}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {〈dom 𝑥, 𝑧〉}:{dom 𝑥}⟶𝐴) | 
| 67 | 63, 65, 66 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {〈dom 𝑥, 𝑧〉}:{dom 𝑥}⟶𝐴) | 
| 68 |  | fdm 6744 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑥:suc 𝑚⟶𝐴 → dom 𝑥 = suc 𝑚) | 
| 69 | 54 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω) | 
| 70 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (dom
𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω)) | 
| 71 | 70 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω)) | 
| 72 | 69, 71 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω) | 
| 73 |  | nnord 7896 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (dom
𝑥 ∈ ω → Ord
dom 𝑥) | 
| 74 |  | ordirr 6401 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (Ord dom
𝑥 → ¬ dom 𝑥 ∈ dom 𝑥) | 
| 75 | 72, 73, 74 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥) | 
| 76 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (dom
𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚)) | 
| 77 | 76 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚)) | 
| 78 | 75, 77 | mtbid 324 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚) | 
| 79 |  | disjsn 4710 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((suc
𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom
𝑥 ∈ suc 𝑚) | 
| 80 | 78, 79 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅) | 
| 81 | 68, 80 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅) | 
| 83 | 57, 67, 82 | fun2d 6771 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴) | 
| 84 |  | sneq 4635 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (dom
𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚}) | 
| 85 | 84 | uneq2d 4167 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (dom
𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚})) | 
| 86 |  | df-suc 6389 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ suc suc
𝑚 = (suc 𝑚 ∪ {suc 𝑚}) | 
| 87 | 85, 86 | eqtr4di 2794 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (dom
𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚) | 
| 88 | 68, 87 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑥:suc 𝑚⟶𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚) | 
| 89 | 88 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚) | 
| 90 | 89 | feq2d 6721 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) | 
| 91 | 83, 90 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴) | 
| 92 | 91 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ 𝐴 → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) | 
| 93 | 92 | adantrd 491 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) | 
| 94 | 93 | a1d 25 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴))) | 
| 95 | 94 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴))) | 
| 96 | 95 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴))) | 
| 97 | 96 | 3imp 1110 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴) | 
| 98 |  | ffun 6738 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑥:suc 𝑚⟶𝐴 → Fun 𝑥) | 
| 99 | 98 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun 𝑥) | 
| 100 | 58, 59 | funsn 6618 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ Fun
{〈dom 𝑥, 𝑧〉} | 
| 101 | 99, 100 | jctir 520 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (Fun 𝑥 ∧ Fun {〈dom 𝑥, 𝑧〉})) | 
| 102 | 59 | dmsnop 6235 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ dom
{〈dom 𝑥, 𝑧〉} = {dom 𝑥} | 
| 103 | 102 | ineq2i 4216 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (dom
𝑥 ∩ dom {〈dom
𝑥, 𝑧〉}) = (dom 𝑥 ∩ {dom 𝑥}) | 
| 104 |  | disjsn 4710 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((dom
𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom
𝑥 ∈ dom 𝑥) | 
| 105 | 75, 104 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅) | 
| 106 | 103, 105 | eqtrid 2788 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {〈dom 𝑥, 𝑧〉}) = ∅) | 
| 107 | 68, 106 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (dom 𝑥 ∩ dom {〈dom 𝑥, 𝑧〉}) = ∅) | 
| 108 |  | funun 6611 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((Fun
𝑥 ∧ Fun {〈dom
𝑥, 𝑧〉}) ∧ (dom 𝑥 ∩ dom {〈dom 𝑥, 𝑧〉}) = ∅) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 109 | 101, 107,
108 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 110 |  | ssun1 4177 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) | 
| 111 | 110 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 112 |  | nnord 7896 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑚 ∈ ω → Ord 𝑚) | 
| 113 |  | 0elsuc 7856 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (Ord
𝑚 → ∅ ∈ suc
𝑚) | 
| 114 | 112, 113 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑚 ∈ ω → ∅
∈ suc 𝑚) | 
| 115 | 114 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ suc 𝑚) | 
| 116 | 68 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑥:suc 𝑚⟶𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚)) | 
| 117 | 116 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚)) | 
| 118 | 115, 117 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ dom 𝑥) | 
| 119 |  | funssfv 6926 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = (𝑥‘∅)) | 
| 120 | 109, 111,
118, 119 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = (𝑥‘∅)) | 
| 121 | 120 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶)) | 
| 122 | 121 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶)) | 
| 123 | 122 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶)) | 
| 124 | 123 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶) | 
| 125 | 124 | adantrl 716 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶) | 
| 126 | 125 | 3adant2 1131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶) | 
| 127 |  | nfra1 3283 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
Ⅎ𝑘∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) | 
| 128 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
Ⅎ𝑘 𝑥:suc 𝑚⟶𝐴 | 
| 129 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
Ⅎ𝑘 𝑚 ∈ ω | 
| 130 | 127, 128,
129 | nf3an 1900 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑘(∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) | 
| 131 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑘 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) | 
| 132 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑘(𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) | 
| 133 | 130, 131,
132 | nf3an 1900 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑘((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) | 
| 134 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ suc 𝑚) | 
| 135 |  | elsuci 6450 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑘 ∈ suc 𝑚 → (𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚)) | 
| 136 |  | rsp 3246 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢
(∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑘 ∈ 𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) | 
| 137 | 136 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝑘 ∈ 𝑚 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) | 
| 138 | 137 | ad2ant2lr 748 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) | 
| 139 | 138 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) | 
| 140 | 109 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 141 | 110 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 142 |  | ordsucelsuc 7843 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ (Ord
𝑚 → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚)) | 
| 143 | 112, 142 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ (𝑚 ∈ ω → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚)) | 
| 144 | 143 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → suc 𝑘 ∈ suc 𝑚) | 
| 145 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ (dom
𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚)) | 
| 146 | 145 | biimparc 479 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((suc
𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥) | 
| 147 | 144, 68, 146 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom 𝑥) | 
| 148 |  | funssfv 6926 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = (𝑥‘suc 𝑘)) | 
| 149 | 140, 141,
147, 148 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = (𝑥‘suc 𝑘)) | 
| 150 | 149 | 3adant2 1131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = (𝑥‘suc 𝑘)) | 
| 151 | 109 | 3adant2 1131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 152 | 110 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 153 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (dom
𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚)) | 
| 154 | 153 | biimparc 479 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥) | 
| 155 | 68, 154 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥) | 
| 156 | 155 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥) | 
| 157 |  | funssfv 6926 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑥 ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) | 
| 158 | 151, 152,
156, 157 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) | 
| 159 | 158 | 3adant1r 1177 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) | 
| 160 | 159 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) = (𝐹‘(𝑥‘𝑘))) | 
| 161 | 150, 160 | eleq12d 2834 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) | 
| 162 | 161 | 3adant2l 1178 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))) | 
| 163 | 139, 162 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))) | 
| 164 | 163 | a1d 25 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 165 | 164 | 3expib 1122 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) | 
| 166 | 165 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑘 ∈ 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) | 
| 167 | 109 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 168 |  | ssun2 4178 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢
{〈dom 𝑥, 𝑧〉} ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) | 
| 169 | 168 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → {〈dom 𝑥, 𝑧〉} ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 170 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚) | 
| 171 | 170 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚)) | 
| 172 | 171 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘) | 
| 173 | 58 | snid 4661 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ dom 𝑥 ∈ {dom 𝑥} | 
| 174 | 173, 102 | eleqtrri 2839 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ dom 𝑥 ∈ dom {〈dom 𝑥, 𝑧〉} | 
| 175 | 172, 174 | eqeltrrdi 2849 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) | 
| 176 | 68, 175 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑘 = 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) | 
| 177 | 176 | 3adant2 1131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) | 
| 178 |  | funssfv 6926 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((Fun
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ {〈dom 𝑥, 𝑧〉} ⊆ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∧ suc 𝑘 ∈ dom {〈dom 𝑥, 𝑧〉}) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = ({〈dom 𝑥, 𝑧〉}‘suc 𝑘)) | 
| 179 | 167, 169,
177, 178 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = ({〈dom 𝑥, 𝑧〉}‘suc 𝑘)) | 
| 180 | 172 | 3adant2 1131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘) | 
| 181 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ (dom
𝑥 = suc 𝑘 → ({〈dom 𝑥, 𝑧〉}‘dom 𝑥) = ({〈dom 𝑥, 𝑧〉}‘suc 𝑘)) | 
| 182 | 58, 59 | fvsn 7202 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢
({〈dom 𝑥, 𝑧〉}‘dom 𝑥) = 𝑧 | 
| 183 | 181, 182 | eqtr3di 2791 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ (dom
𝑥 = suc 𝑘 → ({〈dom 𝑥, 𝑧〉}‘suc 𝑘) = 𝑧) | 
| 184 | 180, 183 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({〈dom 𝑥, 𝑧〉}‘suc 𝑘) = 𝑧) | 
| 185 | 68, 184 | syl3an3 1165 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({〈dom 𝑥, 𝑧〉}‘suc 𝑘) = 𝑧) | 
| 186 | 179, 185 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = 𝑧) | 
| 187 | 186 | 3expa 1118 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = 𝑧) | 
| 188 | 187 | 3adant2 1131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) = 𝑧) | 
| 189 | 158 | 3adant1l 1176 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑘)) | 
| 190 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ (𝑘 = 𝑚 → (𝑥‘𝑘) = (𝑥‘𝑚)) | 
| 191 | 190 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (𝑥‘𝑘) = (𝑥‘𝑚)) | 
| 192 | 191 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘𝑘) = (𝑥‘𝑚)) | 
| 193 | 189, 192 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘) = (𝑥‘𝑚)) | 
| 194 | 193 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) = (𝐹‘(𝑥‘𝑚))) | 
| 195 | 188, 194 | eleq12d 2834 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))) | 
| 196 | 195 | 3adant2l 1178 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))) | 
| 197 | 196 | biimprd 248 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 198 | 197 | 3expib 1122 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) | 
| 199 | 198 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) | 
| 200 | 166, 199 | jaoi 857 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) | 
| 201 | 135, 200 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) | 
| 202 | 201 | com3r 87 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) | 
| 203 | 134, 202 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) | 
| 204 | 203 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))))) | 
| 205 | 204 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑘 ∈ suc 𝑚 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))))) | 
| 206 | 205 | 3impd 1348 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑘 ∈ suc 𝑚 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) | 
| 207 | 206 | impd 410 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈ suc 𝑚 → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 208 | 207 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 209 | 208 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 210 | 133, 209 | ralrimi 3256 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))) | 
| 211 |  | suceq 6449 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚) | 
| 212 | 211 | feq2d 6721 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑝 = suc 𝑚 → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ↔ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴)) | 
| 213 |  | raleq 3322 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑝 = suc 𝑚 → (∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 214 | 212, 213 | 3anbi13d 1439 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑝 = suc 𝑚 → (((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))) ↔ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘))))) | 
| 215 | 214 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((suc
𝑚 ∈ ω ∧
((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 216 | 56, 97, 126, 210, 215 | syl13anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 217 |  | snex 5435 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
{〈dom 𝑥, 𝑧〉} ∈
V | 
| 218 | 32, 217 | unex 7765 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ V | 
| 219 | 22, 23, 218 | axdc3lem3 10493 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {〈dom 𝑥, 𝑧〉})‘𝑘)))) | 
| 220 | 216, 219 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆) | 
| 221 | 220 | 3coml 1127 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆) | 
| 222 | 221 | 3exp 1119 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆))) | 
| 223 | 222 | expd 415 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → (𝑧 ∈ 𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)))) | 
| 224 | 53, 223 | sylcom 30 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)))) | 
| 225 | 224 | 3impd 1348 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)) | 
| 226 | 225 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚⟶𝐴 → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆))) | 
| 227 | 226 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥:suc 𝑚⟶𝐴 → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆))) | 
| 228 | 49, 227 | mpdi 45 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆)) | 
| 229 | 228 | imp 406 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆) | 
| 230 |  | resundir 6011 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥)) | 
| 231 |  | frel 6740 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥:suc 𝑚⟶𝐴 → Rel 𝑥) | 
| 232 |  | resdm 6043 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (Rel
𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥) | 
| 233 | 231, 232 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥) | 
| 234 | 233 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥) | 
| 235 | 68, 72 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → dom 𝑥 ∈ ω) | 
| 236 | 73, 74 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (dom
𝑥 ∈ ω →
¬ dom 𝑥 ∈ dom
𝑥) | 
| 237 |  | incom 4208 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ({dom
𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥}) | 
| 238 | 237 | eqeq1i 2741 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (({dom
𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅) | 
| 239 | 58, 59 | fnsn 6623 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
{〈dom 𝑥, 𝑧〉} Fn {dom 𝑥} | 
| 240 |  | fnresdisj 6687 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
({〈dom 𝑥, 𝑧〉} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅)) | 
| 241 | 239, 240 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (({dom
𝑥} ∩ dom 𝑥) = ∅ ↔ ({〈dom
𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) | 
| 242 | 238, 241,
104 | 3bitr3ri 302 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (¬
dom 𝑥 ∈ dom 𝑥 ↔ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) | 
| 243 | 236, 242 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (dom
𝑥 ∈ ω →
({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) | 
| 244 | 235, 243 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥) = ∅) | 
| 245 | 234, 244 | uneq12d 4168 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥)) = (𝑥 ∪ ∅)) | 
| 246 |  | un0 4393 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∪ ∅) = 𝑥 | 
| 247 | 245, 246 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({〈dom 𝑥, 𝑧〉} ↾ dom 𝑥)) = 𝑥) | 
| 248 | 230, 247 | eqtrid 2788 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) | 
| 249 | 248 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) | 
| 250 | 249 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) | 
| 251 | 250 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) | 
| 252 | 251 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥) | 
| 253 | 102 | uneq2i 4164 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (dom
𝑥 ∪ dom {〈dom
𝑥, 𝑧〉}) = (dom 𝑥 ∪ {dom 𝑥}) | 
| 254 |  | dmun 5920 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ dom
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = (dom 𝑥 ∪ dom {〈dom 𝑥, 𝑧〉}) | 
| 255 |  | df-suc 6389 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ suc dom
𝑥 = (dom 𝑥 ∪ {dom 𝑥}) | 
| 256 | 253, 254,
255 | 3eqtr4i 2774 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom
(𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 | 
| 257 | 252, 256 | jctil 519 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥)) | 
| 258 |  | dmeq 5913 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → dom 𝑦 = dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉})) | 
| 259 | 258 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥)) | 
| 260 |  | reseq1 5990 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥)) | 
| 261 | 260 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥)) | 
| 262 | 259, 261 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥))) | 
| 263 | 262 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {〈dom 𝑥, 𝑧〉}) = suc dom 𝑥 ∧ ((𝑥 ∪ {〈dom 𝑥, 𝑧〉}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) | 
| 264 | 229, 257,
263 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) | 
| 265 | 264 | 3exp2 1354 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))) | 
| 266 | 265 | exlimdv 1932 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))) | 
| 267 | 266 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))) | 
| 268 | 48, 267 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) | 
| 269 | 268 | com3r 87 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) | 
| 270 | 34, 269 | mpan2d 694 | . . . . . . . . . . . . . . 15
⊢
((∀𝑘 ∈
𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) | 
| 271 | 270 | com3r 87 | . . . . . . . . . . . . . 14
⊢ ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) | 
| 272 | 271 | 3expd 1353 | . . . . . . . . . . . . 13
⊢ ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))) | 
| 273 | 272 | com3r 87 | . . . . . . . . . . . 12
⊢ (𝑥:suc 𝑚⟶𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))) | 
| 274 | 273 | 3imp 1110 | . . . . . . . . . . 11
⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) | 
| 275 | 274 | com12 32 | . . . . . . . . . 10
⊢ (𝑚 ∈ ω → ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))) | 
| 276 | 275 | rexlimiv 3147 | . . . . . . . . 9
⊢
(∃𝑚 ∈
ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))) | 
| 277 | 33, 276 | sylbi 217 | . . . . . . . 8
⊢ (𝑥 ∈ 𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))) | 
| 278 | 277 | impcom 407 | . . . . . . 7
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) | 
| 279 |  | rabn0 4388 | . . . . . . 7
⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)) | 
| 280 | 278, 279 | sylibr 234 | . . . . . 6
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅) | 
| 281 | 28 | rabex 5338 | . . . . . . . 8
⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V | 
| 282 | 281 | elsn 4640 | . . . . . . 7
⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅) | 
| 283 | 282 | necon3bbii 2987 | . . . . . 6
⊢ (¬
{𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅) | 
| 284 | 280, 283 | sylibr 234 | . . . . 5
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅}) | 
| 285 | 31, 284 | eldifd 3961 | . . . 4
⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅})) | 
| 286 |  | axdc3lem4.3 | . . . 4
⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)}) | 
| 287 | 285, 286 | fmptd 7133 | . . 3
⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) | 
| 288 | 28 | axdc2 10490 | . . 3
⊢ ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) | 
| 289 | 27, 287, 288 | syl2an 596 | . 2
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) | 
| 290 | 22, 23, 286 | axdc3lem2 10492 | . 2
⊢
(∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) | 
| 291 | 289, 290 | syl 17 | 1
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))) |