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

Theorem axdc3lem4 9864
 Description: Lemma for axdc3 9865. 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 9857 (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 9857 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 9860. See axdc3lem2 9862 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 7581 . . . . . 6 ∅ ∈ ω
2 eqid 2798 . . . . . . . . . 10 {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3 fsng 6876 . . . . . . . . . . 11 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
41, 3mpan 689 . . . . . . . . . 10 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
52, 4mpbiri 261 . . . . . . . . 9 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6 snssi 4701 . . . . . . . . 9 (𝐶𝐴 → {𝐶} ⊆ 𝐴)
75, 6fssd 6502 . . . . . . . 8 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8 suc0 6233 . . . . . . . . 9 suc ∅ = {∅}
98feq2i 6479 . . . . . . . 8 ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
107, 9sylibr 237 . . . . . . 7 (𝐶𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11 fvsng 6919 . . . . . . . 8 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
121, 11mpan 689 . . . . . . 7 (𝐶𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13 ral0 4414 . . . . . . . 8 𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
1413a1i 11 . . . . . . 7 (𝐶𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
1510, 12, 143jca 1125 . . . . . 6 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16 suceq 6224 . . . . . . . . 9 (𝑚 = ∅ → suc 𝑚 = suc ∅)
1716feq2d 6473 . . . . . . . 8 (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18 raleq 3358 . . . . . . . 8 (𝑚 = ∅ → (∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
1917, 183anbi13d 1435 . . . . . . 7 (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
2019rspcev 3571 . . . . . 6 ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
211, 15, 20sylancr 590 . . . . 5 (𝐶𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22 axdc3lem4.1 . . . . . 6 𝐴 ∈ V
23 axdc3lem4.2 . . . . . 6 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
24 snex 5297 . . . . . 6 {⟨∅, 𝐶⟩} ∈ V
2522, 23, 24axdc3lem3 9863 . . . . 5 ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
2621, 25sylibr 237 . . . 4 (𝐶𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
2726ne0d 4251 . . 3 (𝐶𝐴𝑆 ≠ ∅)
2822, 23axdc3lem 9861 . . . . . . 7 𝑆 ∈ V
29 ssrab2 4007 . . . . . . 7 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
3028, 29elpwi2 5213 . . . . . 6 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
3130a1i 11 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
32 vex 3444 . . . . . . . . . 10 𝑥 ∈ V
3322, 23, 32axdc3lem3 9863 . . . . . . . . 9 (𝑥𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
34 simp2 1134 . . . . . . . . . . . . . . . 16 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → 𝑥:suc 𝑚𝐴)
35 vex 3444 . . . . . . . . . . . . . . . . . . . . . 22 𝑚 ∈ V
3635sucid 6238 . . . . . . . . . . . . . . . . . . . . 21 𝑚 ∈ suc 𝑚
37 ffvelrn 6826 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑥𝑚) ∈ 𝐴)
3836, 37mpan2 690 . . . . . . . . . . . . . . . . . . . 20 (𝑥:suc 𝑚𝐴 → (𝑥𝑚) ∈ 𝐴)
39 ffvelrn 6826 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥𝑚) ∈ 𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
4038, 39sylan2 595 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
41 eldifn 4055 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥𝑚)) ∈ {∅})
42 fvex 6658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘(𝑥𝑚)) ∈ V
4342elsn 4540 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) = ∅)
4443necon3bbii 3034 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) ≠ ∅)
45 n0 4260 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹‘(𝑥𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4644, 45bitri 278 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4741, 46sylib 221 . . . . . . . . . . . . . . . . . . 19 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4840, 47syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
49 simp32 1207 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → 𝑥:suc 𝑚𝐴)
50 eldifi 4054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴)
51 elelpwi 4509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴) → 𝑧𝐴)
5251expcom 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
5340, 50, 523syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
54 peano2 7582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ ω → suc 𝑚 ∈ ω)
55543ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → suc 𝑚 ∈ ω)
56553ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
57 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑥:suc 𝑚𝐴)
5832dmex 7598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 dom 𝑥 ∈ V
59 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 𝑧 ∈ V
60 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
61 fsng 6876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
6260, 61mpbiri 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
6358, 59, 62mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
64 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑧𝐴)
6564snssd 4702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {𝑧} ⊆ 𝐴)
66 fss 6501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
6763, 65, 66sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
68 fdm 6495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → dom 𝑥 = suc 𝑚)
6954adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
70 eleq1 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7170adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7269, 71mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
73 nnord 7568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 ∈ ω → Ord dom 𝑥)
74 ordirr 6177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
7572, 73, 743syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
76 eleq2 2878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
7776adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
7875, 77mtbid 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
79 disjsn 4607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
8078, 79sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8168, 80sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8281adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8357, 67, 82fun2d 6516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
84 sneq 4535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
8584uneq2d 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
86 df-suc 6165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
8785, 86eqtr4di 2851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
8868, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
8988ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
9089feq2d 6473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9183, 90mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
9291ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9392adantrd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9493a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
9594ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
96953adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
97963imp 1108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
98 ffun 6490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → Fun 𝑥)
9998adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun 𝑥)
10058, 59funsn 6377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Fun {⟨dom 𝑥, 𝑧⟩}
10199, 100jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
10259dmsnop 6040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
103102ineq2i 4136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
104 disjsn 4607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
10575, 104sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
106103, 105syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
10768, 106sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
108 funun 6370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
109101, 107, 108syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
110 ssun1 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112 nnord 7568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑚 ∈ ω → Ord 𝑚)
113 0elsuc 7530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (Ord 𝑚 → ∅ ∈ suc 𝑚)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
115114adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ suc 𝑚)
11668eleq2d 2875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
117116adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
118115, 117mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ dom 𝑥)
119 funssfv 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
120109, 111, 118, 119syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
121120eqeq1d 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
122121ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
1231223adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
124123biimpar 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
125124adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
1261253adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
127 nfra1 3183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))
128 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑥:suc 𝑚𝐴
129 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑚 ∈ ω
130127, 128, 129nf3an 1902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)
131 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘 𝑧 ∈ (𝐹‘(𝑥𝑚))
132 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)
133130, 131, 132nf3an 1902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑘((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶))
134 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑘 ∈ suc 𝑚)
135 elsuci 6225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 ∈ suc 𝑚 → (𝑘𝑚𝑘 = 𝑚))
136 rsp 3170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑘𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
137136impcom 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑘𝑚 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
138137ad2ant2lr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
1391383adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
140109adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
141110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
142 ordsucelsuc 7517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (Ord 𝑚 → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
143112, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (𝑚 ∈ ω → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
144143biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘𝑚) → suc 𝑘 ∈ suc 𝑚)
145 eleq2 2878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
146145biimparc 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
147144, 68, 146syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom 𝑥)
148 funssfv 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
149140, 141, 147, 148syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1501493adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1511093adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
152110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
153 eleq2 2878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥𝑘 ∈ suc 𝑚))
154153biimparc 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
15568, 154sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
1561553adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
157 funssfv 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
158151, 152, 156, 157syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
1591583adant1r 1174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
160159fveq2d 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑘)))
161150, 160eleq12d 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
1621613adant2l 1175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
163139, 162mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
164163a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
1651643expib 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ 𝑘𝑚) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
166165expcom 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
1671093adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
168 ssun2 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
169168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
170 suceq 6224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
171170eqeq2d 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
172171biimpar 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
17358snid 4561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 dom 𝑥 ∈ {dom 𝑥}
174173, 102eleqtrri 2889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
175172, 174eqeltrrdi 2899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
17668, 175sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
1771763adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
178 funssfv 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
179167, 169, 177, 178syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
1801723adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
18158, 59fvsn 6920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
182 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
183181, 182syl5reqr 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
184180, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
18568, 184syl3an3 1162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
186179, 185eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1871863expa 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1881873adant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1891583adant1l 1173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
190 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (𝑘 = 𝑚 → (𝑥𝑘) = (𝑥𝑚))
191190adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω) → (𝑥𝑘) = (𝑥𝑚))
1921913ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝑥𝑘) = (𝑥𝑚))
193189, 192eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑚))
194193fveq2d 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑚)))
195188, 194eleq12d 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
1961953adant2l 1175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
197196biimprd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
1981973expib 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑘 = 𝑚𝑚 ∈ ω) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
199198ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
200166, 199jaoi 854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205204expcom 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ suc 𝑚 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
2062053impd 1345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ suc 𝑚 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207206impd 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ suc 𝑚 → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
208207com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
2092083adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
210133, 209ralrimi 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
211 suceq 6224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
212211feq2d 6473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
213 raleq 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → (∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
214212, 2133anbi13d 1435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
215214rspcev 3571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
21656, 97, 126, 210, 215syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217 snex 5297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} ∈ V
21832, 217unex 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
21922, 23, 218axdc3lem3 9863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220216, 219sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2212203coml 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2222213exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
223222expd 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → (𝑧𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
22453, 223sylcom 30 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
2252243impd 1345 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
226225ex 416 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚𝐴 → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
227226com23 86 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥:suc 𝑚𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
22849, 227mpdi 45 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229228imp 410 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
230 resundir 5833 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
231 frel 6492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥:suc 𝑚𝐴 → Rel 𝑥)
232 resdm 5863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
233231, 232syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥:suc 𝑚𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
234233adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
23568, 72sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → dom 𝑥 ∈ ω)
23673, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
237 incom 4128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
238237eqeq1i 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
23958, 59fnsn 6382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
240 fnresdisj 6439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
241239, 240ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
242238, 241, 1043bitr3ri 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
243236, 242sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
244235, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245234, 244uneq12d 4091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
246 un0 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∪ ∅) = 𝑥
247245, 246eqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
248230, 247syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
249248ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2502493adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2512503ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252251adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253102uneq2i 4087 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
254 dmun 5743 . . . . . . . . . . . . . . . . . . . . . . . 24 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
255 df-suc 6165 . . . . . . . . . . . . . . . . . . . . . . . 24 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
256253, 254, 2553eqtr4i 2831 . . . . . . . . . . . . . . . . . . . . . . 23 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
257252, 256jctil 523 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
258 dmeq 5736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
259258eqeq1d 2800 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
260 reseq1 5812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
261260eqeq1d 2800 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
262259, 261anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
263262rspcev 3571 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
264229, 257, 263syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
2652643exp2 1351 . . . . . . . . . . . . . . . . . . . 20 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
266265exlimdv 1934 . . . . . . . . . . . . . . . . . . 19 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
267266adantr 484 . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . 15 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
271270com3r 87 . . . . . . . . . . . . . 14 ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
2722713expd 1350 . . . . . . . . . . . . 13 ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
273272com3r 87 . . . . . . . . . . . 12 (𝑥:suc 𝑚𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
2742733imp 1108 . . . . . . . . . . 11 ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275274com12 32 . . . . . . . . . 10 (𝑚 ∈ ω → ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
276275rexlimiv 3239 . . . . . . . . 9 (∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
27733, 276sylbi 220 . . . . . . . 8 (𝑥𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
278277impcom 411 . . . . . . 7 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
279 rabn0 4293 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
280278, 279sylibr 237 . . . . . 6 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
28128rabex 5199 . . . . . . . 8 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
282281elsn 4540 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
283282necon3bbii 3034 . . . . . 6 (¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284280, 283sylibr 237 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
28531, 284eldifd 3892 . . . 4 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
286 axdc3lem4.3 . . . 4 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
287285, 286fmptd 6855 . . 3 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
28828axdc2 9860 . . 3 ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
28927, 287, 288syl2an 598 . 2 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
29022, 23, 286axdc3lem2 9862 . 2 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
291289, 290syl 17 1 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ⟨cop 4531   ↦ cmpt 5110  dom cdm 5519   ↾ cres 5521  Rel wrel 5524  Ord word 6158  suc csuc 6161  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  ωcom 7560 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-dc 9857 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-om 7561  df-1o 8085 This theorem is referenced by:  axdc3  9865
 Copyright terms: Public domain W3C validator