MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axdc3lem4 Structured version   Visualization version   GIF version

Theorem axdc3lem4 10490
Description: Lemma for axdc3 10491. We have constructed a "candidate set" 𝑆, which consists of all finite sequences 𝑠 that satisfy our property of interest, namely 𝑠(𝑥 + 1) ∈ 𝐹(𝑠(𝑥)) on its domain, but with the added constraint that 𝑠(0) = 𝐶. These sets are possible "initial segments" of the infinite sequence satisfying these constraints, but we can leverage the standard ax-dc 10483 (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely (𝑛):𝑚𝐴 (for some integer 𝑚). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc 10483 yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that 𝑆 is nonempty, and that 𝐺 always maps to a nonempty subset of 𝑆, so that we can apply axdc2 10486. See axdc3lem2 10488 for the rest of the proof. (Contributed by Mario Carneiro, 27-Jan-2013.)
Hypotheses
Ref Expression
axdc3lem4.1 𝐴 ∈ V
axdc3lem4.2 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
axdc3lem4.3 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
Assertion
Ref Expression
axdc3lem4 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Distinct variable groups:   𝐴,𝑔,𝑘   𝐴,𝑛,𝑥,𝑘,𝑠   𝐶,𝑔,𝑘   𝐶,𝑛,𝑠   𝑔,𝐹,𝑘   𝑛,𝐹,𝑥,𝑠   𝑘,𝐺   𝑆,𝑘,𝑠,𝑥   𝑦,𝑆,𝑥   𝑛,𝑠
Allowed substitution hints:   𝐴(𝑦)   𝐶(𝑥,𝑦)   𝑆(𝑔,𝑛)   𝐹(𝑦)   𝐺(𝑥,𝑦,𝑔,𝑛,𝑠)

Proof of Theorem axdc3lem4
Dummy variables 𝑚 𝑝 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 7910 . . . . . 6 ∅ ∈ ω
2 eqid 2734 . . . . . . . . . 10 {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3 fsng 7156 . . . . . . . . . . 11 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
41, 3mpan 690 . . . . . . . . . 10 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
52, 4mpbiri 258 . . . . . . . . 9 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6 snssi 4812 . . . . . . . . 9 (𝐶𝐴 → {𝐶} ⊆ 𝐴)
75, 6fssd 6753 . . . . . . . 8 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8 suc0 6460 . . . . . . . . 9 suc ∅ = {∅}
98feq2i 6728 . . . . . . . 8 ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
107, 9sylibr 234 . . . . . . 7 (𝐶𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11 fvsng 7199 . . . . . . . 8 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
121, 11mpan 690 . . . . . . 7 (𝐶𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13 ral0 4518 . . . . . . . 8 𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
1413a1i 11 . . . . . . 7 (𝐶𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
1510, 12, 143jca 1127 . . . . . 6 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16 suceq 6451 . . . . . . . . 9 (𝑚 = ∅ → suc 𝑚 = suc ∅)
1716feq2d 6722 . . . . . . . 8 (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18 raleq 3320 . . . . . . . 8 (𝑚 = ∅ → (∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
1917, 183anbi13d 1437 . . . . . . 7 (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
2019rspcev 3621 . . . . . 6 ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
211, 15, 20sylancr 587 . . . . 5 (𝐶𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22 axdc3lem4.1 . . . . . 6 𝐴 ∈ V
23 axdc3lem4.2 . . . . . 6 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
24 snex 5441 . . . . . 6 {⟨∅, 𝐶⟩} ∈ V
2522, 23, 24axdc3lem3 10489 . . . . 5 ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
2621, 25sylibr 234 . . . 4 (𝐶𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
2726ne0d 4347 . . 3 (𝐶𝐴𝑆 ≠ ∅)
2822, 23axdc3lem 10487 . . . . . . 7 𝑆 ∈ V
29 ssrab2 4089 . . . . . . 7 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
3028, 29elpwi2 5340 . . . . . 6 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
3130a1i 11 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
32 vex 3481 . . . . . . . . . 10 𝑥 ∈ V
3322, 23, 32axdc3lem3 10489 . . . . . . . . 9 (𝑥𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
34 simp2 1136 . . . . . . . . . . . . . . . 16 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → 𝑥:suc 𝑚𝐴)
35 vex 3481 . . . . . . . . . . . . . . . . . . . . . 22 𝑚 ∈ V
3635sucid 6467 . . . . . . . . . . . . . . . . . . . . 21 𝑚 ∈ suc 𝑚
37 ffvelcdm 7100 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑥𝑚) ∈ 𝐴)
3836, 37mpan2 691 . . . . . . . . . . . . . . . . . . . 20 (𝑥:suc 𝑚𝐴 → (𝑥𝑚) ∈ 𝐴)
39 ffvelcdm 7100 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥𝑚) ∈ 𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
4038, 39sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
41 eldifn 4141 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥𝑚)) ∈ {∅})
42 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘(𝑥𝑚)) ∈ V
4342elsn 4645 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) = ∅)
4443necon3bbii 2985 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) ≠ ∅)
45 n0 4358 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹‘(𝑥𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4644, 45bitri 275 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4741, 46sylib 218 . . . . . . . . . . . . . . . . . . 19 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4840, 47syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
49 simp32 1209 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → 𝑥:suc 𝑚𝐴)
50 eldifi 4140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴)
51 elelpwi 4614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴) → 𝑧𝐴)
5251expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
5340, 50, 523syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
54 peano2 7912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ ω → suc 𝑚 ∈ ω)
55543ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → suc 𝑚 ∈ ω)
56553ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
57 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑥:suc 𝑚𝐴)
5832dmex 7931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 dom 𝑥 ∈ V
59 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 𝑧 ∈ V
60 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
61 fsng 7156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
6260, 61mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
6358, 59, 62mp2an 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
64 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑧𝐴)
6564snssd 4813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {𝑧} ⊆ 𝐴)
66 fss 6752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
6763, 65, 66sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
68 fdm 6745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → dom 𝑥 = suc 𝑚)
6954adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
70 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7170adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7269, 71mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
73 nnord 7894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 ∈ ω → Ord dom 𝑥)
74 ordirr 6403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
7572, 73, 743syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
76 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
7776adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
7875, 77mtbid 324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
79 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
8078, 79sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8168, 80sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8281adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8357, 67, 82fun2d 6772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
84 sneq 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
8584uneq2d 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
86 df-suc 6391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
8785, 86eqtr4di 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
8868, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
8988ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
9089feq2d 6722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9183, 90mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
9291ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9392adantrd 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9493a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
9594ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
96953adant1 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
97963imp 1110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
98 ffun 6739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → Fun 𝑥)
9998adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun 𝑥)
10058, 59funsn 6620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Fun {⟨dom 𝑥, 𝑧⟩}
10199, 100jctir 520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
10259dmsnop 6237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
103102ineq2i 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
104 disjsn 4715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
10575, 104sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
106103, 105eqtrid 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
10768, 106sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
108 funun 6613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
109101, 107, 108syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
110 ssun1 4187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112 nnord 7894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑚 ∈ ω → Ord 𝑚)
113 0elsuc 7854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (Ord 𝑚 → ∅ ∈ suc 𝑚)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
115114adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ suc 𝑚)
11668eleq2d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
117116adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
118115, 117mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ dom 𝑥)
119 funssfv 6927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
120109, 111, 118, 119syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
121120eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
122121ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
1231223adant1 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
124123biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
125124adantrl 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
1261253adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
127 nfra1 3281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))
128 nfv 1911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑥:suc 𝑚𝐴
129 nfv 1911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑚 ∈ ω
130127, 128, 129nf3an 1898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)
131 nfv 1911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘 𝑧 ∈ (𝐹‘(𝑥𝑚))
132 nfv 1911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)
133130, 131, 132nf3an 1898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑘((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶))
134 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑘 ∈ suc 𝑚)
135 elsuci 6452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 ∈ suc 𝑚 → (𝑘𝑚𝑘 = 𝑚))
136 rsp 3244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑘𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
137136impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑘𝑚 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
138137ad2ant2lr 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
1391383adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
140109adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
141110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
142 ordsucelsuc 7841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (Ord 𝑚 → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
143112, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (𝑚 ∈ ω → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
144143biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘𝑚) → suc 𝑘 ∈ suc 𝑚)
145 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
146145biimparc 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
147144, 68, 146syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom 𝑥)
148 funssfv 6927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
149140, 141, 147, 148syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1501493adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1511093adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
152110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
153 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥𝑘 ∈ suc 𝑚))
154153biimparc 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
15568, 154sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
1561553adant1 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
157 funssfv 6927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
158151, 152, 156, 157syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
1591583adant1r 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
160159fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑘)))
161150, 160eleq12d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
1621613adant2l 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
163139, 162mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
164163a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
1651643expib 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ 𝑘𝑚) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
166165expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
1671093adant1 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
168 ssun2 4188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
169168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
170 suceq 6451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
171170eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
172171biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
17358snid 4666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 dom 𝑥 ∈ {dom 𝑥}
174173, 102eleqtrri 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
175172, 174eqeltrrdi 2847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
17668, 175sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
1771763adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
178 funssfv 6927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
179167, 169, 177, 178syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
1801723adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
181 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
18258, 59fvsn 7200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
183181, 182eqtr3di 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
184180, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
18568, 184syl3an3 1164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
186179, 185eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1871863expa 1117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1881873adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1891583adant1l 1175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
190 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (𝑘 = 𝑚 → (𝑥𝑘) = (𝑥𝑚))
191190adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω) → (𝑥𝑘) = (𝑥𝑚))
1921913ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝑥𝑘) = (𝑥𝑚))
193189, 192eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑚))
194193fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑚)))
195188, 194eleq12d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
1961953adant2l 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
197196biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
1981973expib 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑘 = 𝑚𝑚 ∈ ω) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
199198ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
200166, 199jaoi 857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑘𝑚𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
201135, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
202201com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
203134, 202mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
204203ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205204expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ suc 𝑚 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
2062053impd 1347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ suc 𝑚 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207206impd 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ suc 𝑚 → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
208207com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
2092083adant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
210133, 209ralrimi 3254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
211 suceq 6451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
212211feq2d 6722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
213 raleq 3320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → (∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
214212, 2133anbi13d 1437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
215214rspcev 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
21656, 97, 126, 210, 215syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217 snex 5441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} ∈ V
21832, 217unex 7762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
21922, 23, 218axdc3lem3 10489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220216, 219sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2212203coml 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2222213exp 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
223222expd 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → (𝑧𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
22453, 223sylcom 30 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
2252243impd 1347 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
226225ex 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚𝐴 → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
227226com23 86 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥:suc 𝑚𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
22849, 227mpdi 45 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229228imp 406 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
230 resundir 6014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
231 frel 6741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥:suc 𝑚𝐴 → Rel 𝑥)
232 resdm 6045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
233231, 232syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥:suc 𝑚𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
234233adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
23568, 72sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → dom 𝑥 ∈ ω)
23673, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
237 incom 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
238237eqeq1i 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
23958, 59fnsn 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
240 fnresdisj 6688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
241239, 240ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
242238, 241, 1043bitr3ri 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
243236, 242sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
244235, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245234, 244uneq12d 4178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
246 un0 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∪ ∅) = 𝑥
247245, 246eqtrdi 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
248230, 247eqtrid 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
249248ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2502493adant1 1129 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2512503ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252251adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253102uneq2i 4174 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
254 dmun 5923 . . . . . . . . . . . . . . . . . . . . . . . 24 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
255 df-suc 6391 . . . . . . . . . . . . . . . . . . . . . . . 24 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
256253, 254, 2553eqtr4i 2772 . . . . . . . . . . . . . . . . . . . . . . 23 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
257252, 256jctil 519 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
258 dmeq 5916 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
259258eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
260 reseq1 5993 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
261260eqeq1d 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
262259, 261anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
263262rspcev 3621 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
264229, 257, 263syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
2652643exp2 1353 . . . . . . . . . . . . . . . . . . . 20 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
266265exlimdv 1930 . . . . . . . . . . . . . . . . . . 19 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
267266adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
26848, 267mpd 15 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
269268com3r 87 . . . . . . . . . . . . . . . 16 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
27034, 269mpan2d 694 . . . . . . . . . . . . . . 15 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
271270com3r 87 . . . . . . . . . . . . . 14 ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
2722713expd 1352 . . . . . . . . . . . . 13 ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
273272com3r 87 . . . . . . . . . . . 12 (𝑥:suc 𝑚𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
2742733imp 1110 . . . . . . . . . . 11 ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275274com12 32 . . . . . . . . . 10 (𝑚 ∈ ω → ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
276275rexlimiv 3145 . . . . . . . . 9 (∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
27733, 276sylbi 217 . . . . . . . 8 (𝑥𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
278277impcom 407 . . . . . . 7 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
279 rabn0 4394 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
280278, 279sylibr 234 . . . . . 6 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
28128rabex 5344 . . . . . . . 8 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
282281elsn 4645 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
283282necon3bbii 2985 . . . . . 6 (¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284280, 283sylibr 234 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
28531, 284eldifd 3973 . . . 4 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
286 axdc3lem4.3 . . . 4 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
287285, 286fmptd 7133 . . 3 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
28828axdc2 10486 . . 3 ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
28927, 287, 288syl2an 596 . 2 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
29022, 23, 286axdc3lem2 10488 . 2 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
291289, 290syl 17 1 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wex 1775  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604  {csn 4630  cop 4636  cmpt 5230  dom cdm 5688  cres 5690  Rel wrel 5693  Ord word 6384  suc csuc 6387  Fun wfun 6556   Fn wfn 6557  wf 6558  cfv 6562  ωcom 7886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-dc 10483
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-om 7887  df-1o 8504
This theorem is referenced by:  axdc3  10491
  Copyright terms: Public domain W3C validator