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

Theorem axdc3lem4 9227
Description: Lemma for axdc3 9228. 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 9220 (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 9220 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 9223. See axdc3lem2 9225 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 7039 . . . . . 6 ∅ ∈ ω
2 eqid 2621 . . . . . . . . . 10 {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3 fsng 6364 . . . . . . . . . . 11 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
41, 3mpan 705 . . . . . . . . . 10 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
52, 4mpbiri 248 . . . . . . . . 9 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6 snssi 4313 . . . . . . . . 9 (𝐶𝐴 → {𝐶} ⊆ 𝐴)
75, 6fssd 6019 . . . . . . . 8 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8 suc0 5763 . . . . . . . . 9 suc ∅ = {∅}
98feq2i 5999 . . . . . . . 8 ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
107, 9sylibr 224 . . . . . . 7 (𝐶𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11 fvsng 6407 . . . . . . . 8 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
121, 11mpan 705 . . . . . . 7 (𝐶𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13 ral0 4053 . . . . . . . 8 𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
1413a1i 11 . . . . . . 7 (𝐶𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
1510, 12, 143jca 1240 . . . . . 6 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16 suceq 5754 . . . . . . . . 9 (𝑚 = ∅ → suc 𝑚 = suc ∅)
1716feq2d 5993 . . . . . . . 8 (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18 raleq 3130 . . . . . . . 8 (𝑚 = ∅ → (∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
1917, 183anbi13d 1398 . . . . . . 7 (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
2019rspcev 3298 . . . . . 6 ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
211, 15, 20sylancr 694 . . . . 5 (𝐶𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22 axdc3lem4.1 . . . . . 6 𝐴 ∈ V
23 axdc3lem4.2 . . . . . 6 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
24 snex 4874 . . . . . 6 {⟨∅, 𝐶⟩} ∈ V
2522, 23, 24axdc3lem3 9226 . . . . 5 ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
2621, 25sylibr 224 . . . 4 (𝐶𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
27 ne0i 3902 . . . 4 ({⟨∅, 𝐶⟩} ∈ 𝑆𝑆 ≠ ∅)
2826, 27syl 17 . . 3 (𝐶𝐴𝑆 ≠ ∅)
29 ssrab2 3671 . . . . . . 7 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
3022, 23axdc3lem 9224 . . . . . . . 8 𝑆 ∈ V
3130elpw2 4793 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆 ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆)
3229, 31mpbir 221 . . . . . 6 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
3332a1i 11 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
34 vex 3192 . . . . . . . . . 10 𝑥 ∈ V
3522, 23, 34axdc3lem3 9226 . . . . . . . . 9 (𝑥𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
36 simp2 1060 . . . . . . . . . . . . . . . 16 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → 𝑥:suc 𝑚𝐴)
37 vex 3192 . . . . . . . . . . . . . . . . . . . . . 22 𝑚 ∈ V
3837sucid 5768 . . . . . . . . . . . . . . . . . . . . 21 𝑚 ∈ suc 𝑚
39 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑥𝑚) ∈ 𝐴)
4038, 39mpan2 706 . . . . . . . . . . . . . . . . . . . 20 (𝑥:suc 𝑚𝐴 → (𝑥𝑚) ∈ 𝐴)
41 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥𝑚) ∈ 𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
4240, 41sylan2 491 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
43 eldifn 3716 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥𝑚)) ∈ {∅})
44 fvex 6163 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘(𝑥𝑚)) ∈ V
4544elsn 4168 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) = ∅)
4645necon3bbii 2837 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) ≠ ∅)
47 n0 3912 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹‘(𝑥𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4846, 47bitri 264 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4943, 48sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
5042, 49syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
51 simp32 1096 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → 𝑥:suc 𝑚𝐴)
52 eldifi 3715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴)
53 elelpwi 4147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴) → 𝑧𝐴)
5453expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
5542, 52, 543syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
56 peano2 7040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ ω → suc 𝑚 ∈ ω)
57563ad2ant3 1082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → suc 𝑚 ∈ ω)
58573ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
59 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑥:suc 𝑚𝐴)
6034dmex 7053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 dom 𝑥 ∈ V
61 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 𝑧 ∈ V
62 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
63 fsng 6364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
6462, 63mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
6560, 61, 64mp2an 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
66 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑧𝐴)
6766snssd 4314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {𝑧} ⊆ 𝐴)
68 fss 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
6965, 67, 68sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
70 fdm 6013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → dom 𝑥 = suc 𝑚)
7156adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
72 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7372adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7471, 73mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
75 nnord 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 ∈ ω → Ord dom 𝑥)
76 ordirr 5705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
7774, 75, 763syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
78 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
7978adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
8077, 79mtbid 314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
81 disjsn 4221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
8280, 81sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8370, 82sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8483adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
85 fun2 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑥:suc 𝑚𝐴 ∧ {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴) ∧ (suc 𝑚 ∩ {dom 𝑥}) = ∅) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
8659, 69, 84, 85syl21anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
87 sneq 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
8887uneq2d 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
89 df-suc 5693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
9088, 89syl6eqr 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
9170, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
9291ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
9392feq2d 5993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9486, 93mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
9594ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9695adantrd 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9796a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
9897ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
99983adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
100993imp 1254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
101 ffun 6010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → Fun 𝑥)
102101adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun 𝑥)
10360, 61funsn 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Fun {⟨dom 𝑥, 𝑧⟩}
104102, 103jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
10561dmsnop 5573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
106105ineq2i 3794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
107 disjsn 4221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
10877, 107sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
109106, 108syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
11070, 109sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
111 funun 5895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112104, 110, 111syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
113 ssun1 3759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
115 nnord 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑚 ∈ ω → Ord 𝑚)
116 0elsuc 6989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (Ord 𝑚 → ∅ ∈ suc 𝑚)
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
118117adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ suc 𝑚)
11970eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
120119adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
121118, 120mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ dom 𝑥)
122 funssfv 6171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
123112, 114, 121, 122syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
124123eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
125124ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
1261253adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
127126biimpar 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
128127adantrl 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
1291283adant2 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
130 nfra1 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))
131 nfv 1840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑥:suc 𝑚𝐴
132 nfv 1840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑚 ∈ ω
133130, 131, 132nf3an 1828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)
134 nfv 1840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘 𝑧 ∈ (𝐹‘(𝑥𝑚))
135 nfv 1840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)
136133, 134, 135nf3an 1828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑘((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶))
137 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑘 ∈ suc 𝑚)
138 elsuci 5755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 ∈ suc 𝑚 → (𝑘𝑚𝑘 = 𝑚))
139 rsp 2924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑘𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
140139impcom 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑘𝑚 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
141140ad2ant2lr 783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
1421413adant3 1079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
143112adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
144113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
145 ordsucelsuc 6976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (Ord 𝑚 → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
146115, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (𝑚 ∈ ω → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
147146biimpa 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘𝑚) → suc 𝑘 ∈ suc 𝑚)
148 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
149148biimparc 504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
150147, 70, 149syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom 𝑥)
151 funssfv 6171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
152143, 144, 150, 151syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1531523adant2 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1541123adant2 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
155113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
156 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥𝑘 ∈ suc 𝑚))
157156biimparc 504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
15870, 157sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
1591583adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
160 funssfv 6171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
161154, 155, 159, 160syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
1621613adant1r 1316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
163162fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑘)))
164153, 163eleq12d 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
1651643adant2l 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
166142, 165mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
167166a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
1681673expib 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ 𝑘𝑚) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
169168expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
1701123adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
171 ssun2 3760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
173 suceq 5754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
174173eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
175174biimpar 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
17660snid 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 dom 𝑥 ∈ {dom 𝑥}
177176, 105eleqtrri 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
178175, 177syl6eqelr 2707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
17970, 178sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
1801793adant2 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
181 funssfv 6171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
182170, 172, 180, 181syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
1831753adant2 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
18460, 61fvsn 6406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
185 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
186184, 185syl5reqr 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
187183, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
18870, 187syl3an3 1358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
189182, 188eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1901893expa 1262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1911903adant2 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1921613adant1l 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
193 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (𝑘 = 𝑚 → (𝑥𝑘) = (𝑥𝑚))
194193adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω) → (𝑥𝑘) = (𝑥𝑚))
1951943ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝑥𝑘) = (𝑥𝑚))
196192, 195eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑚))
197196fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑚)))
198191, 197eleq12d 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
1991983adant2l 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
200199biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
2012003expib 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑘 = 𝑚𝑚 ∈ ω) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
202201ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
203169, 202jaoi 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑘𝑚𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
204138, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205204com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
206137, 205mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207206ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
208207expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ suc 𝑚 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
2092083impd 1278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ suc 𝑚 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
210209impd 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ suc 𝑚 → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
211210com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
2122113adant3 1079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
213136, 212ralrimi 2952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
214 suceq 5754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
215214feq2d 5993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
216 raleq 3130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → (∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217215, 2163anbi13d 1398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
218217rspcev 3298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
21958, 100, 129, 213, 218syl13anc 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220 snex 4874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} ∈ V
22134, 220unex 6916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
22222, 23, 221axdc3lem3 9226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
223219, 222sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2242233coml 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2252243exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
226225expd 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → (𝑧𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
22755, 226sylcom 30 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
2282273impd 1278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229228ex 450 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚𝐴 → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
230229com23 86 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥:suc 𝑚𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
23151, 230mpdi 45 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
232231imp 445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
233 resundir 5375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
234 frel 6012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥:suc 𝑚𝐴 → Rel 𝑥)
235 resdm 5405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
236234, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥:suc 𝑚𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
237236adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
23870, 74sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → dom 𝑥 ∈ ω)
23975, 76syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
240 incom 3788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
241240eqeq1i 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
24260, 61fnsn 5909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
243 fnresdisj 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
244242, 243ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245241, 244, 1073bitr3ri 291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
246239, 245sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
247238, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
248237, 247uneq12d 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
249 un0 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∪ ∅) = 𝑥
250248, 249syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
251233, 250syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252251ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2532523adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2542533ad2ant3 1082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
255254adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
256105uneq2i 3747 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
257 dmun 5296 . . . . . . . . . . . . . . . . . . . . . . . 24 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
258 df-suc 5693 . . . . . . . . . . . . . . . . . . . . . . . 24 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
259256, 257, 2583eqtr4i 2653 . . . . . . . . . . . . . . . . . . . . . . 23 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
260255, 259jctil 559 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
261 dmeq 5289 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
262261eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
263 reseq1 5355 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
264263eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
265262, 264anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
266265rspcev 3298 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
267232, 260, 266syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
2682673exp2 1282 . . . . . . . . . . . . . . . . . . . 20 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
269268exlimdv 1858 . . . . . . . . . . . . . . . . . . 19 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
270269adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
27150, 270mpd 15 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
272271com3r 87 . . . . . . . . . . . . . . . 16 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
27336, 272mpan2d 709 . . . . . . . . . . . . . . 15 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
274273com3r 87 . . . . . . . . . . . . . 14 ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
2752743expd 1281 . . . . . . . . . . . . 13 ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
276275com3r 87 . . . . . . . . . . . 12 (𝑥:suc 𝑚𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
2772763imp 1254 . . . . . . . . . . 11 ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
278277com12 32 . . . . . . . . . 10 (𝑚 ∈ ω → ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
279278rexlimiv 3021 . . . . . . . . 9 (∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
28035, 279sylbi 207 . . . . . . . 8 (𝑥𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
281280impcom 446 . . . . . . 7 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
282 rabn0 3937 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
283281, 282sylibr 224 . . . . . 6 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
28430rabex 4778 . . . . . . . 8 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
285284elsn 4168 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
286285necon3bbii 2837 . . . . . 6 (¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
287283, 286sylibr 224 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
28833, 287eldifd 3570 . . . 4 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
289 axdc3lem4.3 . . . 4 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
290288, 289fmptd 6346 . . 3 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
29130axdc2 9223 . . 3 ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
29228, 290, 291syl2an 494 . 2 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
29322, 23, 289axdc3lem2 9225 . 2 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
294292, 293syl 17 1 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135  {csn 4153  cop 4159  cmpt 4678  dom cdm 5079  cres 5081  Rel wrel 5084  Ord word 5686  suc csuc 5689  Fun wfun 5846   Fn wfn 5847  wf 5848  cfv 5852  ωcom 7019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-dc 9220
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-om 7020  df-1o 7512
This theorem is referenced by:  axdc3  9228
  Copyright terms: Public domain W3C validator