MPE Home 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