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

Theorem axdc3lem4 10494
Description: Lemma for axdc3 10495. 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 10487 (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 10487 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 10490. See axdc3lem2 10492 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 7911 . . . . . 6 ∅ ∈ ω
2 eqid 2736 . . . . . . . . . 10 {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3 fsng 7156 . . . . . . . . . . 11 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
41, 3mpan 690 . . . . . . . . . 10 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
52, 4mpbiri 258 . . . . . . . . 9 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6 snssi 4807 . . . . . . . . 9 (𝐶𝐴 → {𝐶} ⊆ 𝐴)
75, 6fssd 6752 . . . . . . . 8 (𝐶𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8 suc0 6458 . . . . . . . . 9 suc ∅ = {∅}
98feq2i 6727 . . . . . . . 8 ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
107, 9sylibr 234 . . . . . . 7 (𝐶𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11 fvsng 7201 . . . . . . . 8 ((∅ ∈ ω ∧ 𝐶𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
121, 11mpan 690 . . . . . . 7 (𝐶𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13 ral0 4512 . . . . . . . 8 𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
1413a1i 11 . . . . . . 7 (𝐶𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
1510, 12, 143jca 1128 . . . . . 6 (𝐶𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16 suceq 6449 . . . . . . . . 9 (𝑚 = ∅ → suc 𝑚 = suc ∅)
1716feq2d 6721 . . . . . . . 8 (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18 raleq 3322 . . . . . . . 8 (𝑚 = ∅ → (∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
1917, 183anbi13d 1439 . . . . . . 7 (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
2019rspcev 3621 . . . . . 6 ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
211, 15, 20sylancr 587 . . . . 5 (𝐶𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22 axdc3lem4.1 . . . . . 6 𝐴 ∈ V
23 axdc3lem4.2 . . . . . 6 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
24 snex 5435 . . . . . 6 {⟨∅, 𝐶⟩} ∈ V
2522, 23, 24axdc3lem3 10493 . . . . 5 ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
2621, 25sylibr 234 . . . 4 (𝐶𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
2726ne0d 4341 . . 3 (𝐶𝐴𝑆 ≠ ∅)
2822, 23axdc3lem 10491 . . . . . . 7 𝑆 ∈ V
29 ssrab2 4079 . . . . . . 7 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
3028, 29elpwi2 5334 . . . . . 6 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
3130a1i 11 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
32 vex 3483 . . . . . . . . . 10 𝑥 ∈ V
3322, 23, 32axdc3lem3 10493 . . . . . . . . 9 (𝑥𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
34 simp2 1137 . . . . . . . . . . . . . . . 16 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → 𝑥:suc 𝑚𝐴)
35 vex 3483 . . . . . . . . . . . . . . . . . . . . . 22 𝑚 ∈ V
3635sucid 6465 . . . . . . . . . . . . . . . . . . . . 21 𝑚 ∈ suc 𝑚
37 ffvelcdm 7100 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥:suc 𝑚𝐴𝑚 ∈ suc 𝑚) → (𝑥𝑚) ∈ 𝐴)
3836, 37mpan2 691 . . . . . . . . . . . . . . . . . . . 20 (𝑥:suc 𝑚𝐴 → (𝑥𝑚) ∈ 𝐴)
39 ffvelcdm 7100 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥𝑚) ∈ 𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
4038, 39sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
41 eldifn 4131 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥𝑚)) ∈ {∅})
42 fvex 6918 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘(𝑥𝑚)) ∈ V
4342elsn 4640 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) = ∅)
4443necon3bbii 2987 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥𝑚)) ≠ ∅)
45 n0 4352 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹‘(𝑥𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4644, 45bitri 275 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐹‘(𝑥𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4741, 46sylib 218 . . . . . . . . . . . . . . . . . . 19 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
4840, 47syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)))
49 simp32 1210 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → 𝑥:suc 𝑚𝐴)
50 eldifi 4130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴)
51 elelpwi 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴) → 𝑧𝐴)
5251expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹‘(𝑥𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
5340, 50, 523syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → 𝑧𝐴))
54 peano2 7913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚 ∈ ω → suc 𝑚 ∈ ω)
55543ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → suc 𝑚 ∈ ω)
56553ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
57 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑥:suc 𝑚𝐴)
5832dmex 7932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 dom 𝑥 ∈ V
59 vex 3483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 𝑧 ∈ V
60 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
61 fsng 7156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
6260, 61mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
6358, 59, 62mp2an 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
64 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → 𝑧𝐴)
6564snssd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {𝑧} ⊆ 𝐴)
66 fss 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
6763, 65, 66sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
68 fdm 6744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → dom 𝑥 = suc 𝑚)
6954adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
70 eleq1 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7170adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
7269, 71mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
73 nnord 7896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 ∈ ω → Ord dom 𝑥)
74 ordirr 6401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
7572, 73, 743syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
76 eleq2 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
7776adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
7875, 77mtbid 324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
79 disjsn 4710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
8078, 79sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8168, 80sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8281adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
8357, 67, 82fun2d 6771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
84 sneq 4635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
8584uneq2d 4167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
86 df-suc 6389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
8785, 86eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
8868, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
8988ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
9089feq2d 6721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9183, 90mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) ∧ 𝑧𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
9291ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9392adantrd 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
9493a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
9594ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
96953adant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)))
97963imp 1110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴)
98 ffun 6738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥:suc 𝑚𝐴 → Fun 𝑥)
9998adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun 𝑥)
10058, 59funsn 6618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Fun {⟨dom 𝑥, 𝑧⟩}
10199, 100jctir 520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
10259dmsnop 6235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
103102ineq2i 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
104 disjsn 4710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
10575, 104sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
106103, 105eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
10768, 106sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
108 funun 6611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
109101, 107, 108syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
110 ssun1 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112 nnord 7896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑚 ∈ ω → Ord 𝑚)
113 0elsuc 7856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (Ord 𝑚 → ∅ ∈ suc 𝑚)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
115114adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ suc 𝑚)
11668eleq2d 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥:suc 𝑚𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
117116adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
118115, 117mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ∅ ∈ dom 𝑥)
119 funssfv 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
120109, 111, 118, 119syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
121120eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
122121ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
1231223adant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
124123biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
125124adantrl 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
1261253adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
127 nfra1 3283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))
128 nfv 1913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑥:suc 𝑚𝐴
129 nfv 1913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑘 𝑚 ∈ ω
130127, 128, 129nf3an 1900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)
131 nfv 1913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘 𝑧 ∈ (𝐹‘(𝑥𝑚))
132 nfv 1913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑘(𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)
133130, 131, 132nf3an 1900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑘((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶))
134 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑘 ∈ suc 𝑚)
135 elsuci 6450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 ∈ suc 𝑚 → (𝑘𝑚𝑘 = 𝑚))
136 rsp 3246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑘𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
137136impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑘𝑚 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
138137ad2ant2lr 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
1391383adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)))
140109adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
141110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
142 ordsucelsuc 7843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (Ord 𝑚 → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
143112, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (𝑚 ∈ ω → (𝑘𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
144143biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘𝑚) → suc 𝑘 ∈ suc 𝑚)
145 eleq2 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
146145biimparc 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
147144, 68, 146syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom 𝑥)
148 funssfv 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
149140, 141, 147, 148syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1501493adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
1511093adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
152110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
153 eleq2 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥𝑘 ∈ suc 𝑚))
154153biimparc 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
15568, 154sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
1561553adant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → 𝑘 ∈ dom 𝑥)
157 funssfv 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
158151, 152, 156, 157syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
1591583adant1r 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
160159fveq2d 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑘)))
161150, 160eleq12d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
1621613adant2l 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))))
163139, 162mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
164163a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑚 ∈ ω ∧ 𝑘𝑚) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
1651643expib 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚 ∈ ω ∧ 𝑘𝑚) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
166165expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
1671093adant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
168 ssun2 4178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
169168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
170 suceq 6449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
171170eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
172171biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
17358snid 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 dom 𝑥 ∈ {dom 𝑥}
174173, 102eleqtrri 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
175172, 174eqeltrrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
17668, 175sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
1771763adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
178 funssfv 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
179167, 169, 177, 178syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
1801723adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
181 fveq2 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
18258, 59fvsn 7202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
183181, 182eqtr3di 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
184180, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ((𝑘 = 𝑚𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
18568, 184syl3an3 1165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
186179, 185eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑘 = 𝑚𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1871863expa 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1881873adant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
1891583adant1l 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑘))
190 fveq2 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (𝑘 = 𝑚 → (𝑥𝑘) = (𝑥𝑚))
191190adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((𝑘 = 𝑚𝑚 ∈ ω) → (𝑥𝑘) = (𝑥𝑚))
1921913ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝑥𝑘) = (𝑥𝑚))
193189, 192eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥𝑚))
194193fveq2d 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥𝑚)))
195188, 194eleq12d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
1961953adant2l 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥𝑚))))
197196biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((𝑘 = 𝑚𝑚 ∈ ω) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
1981973expib 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑘 = 𝑚𝑚 ∈ ω) → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
199198ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
200166, 199jaoi 857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑘𝑚𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
201135, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
202201com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
203134, 202mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
204203ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205204expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ suc 𝑚 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
2062053impd 1348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ suc 𝑚 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207206impd 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ suc 𝑚 → (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
208207com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
2092083adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
210133, 209ralrimi 3256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
211 suceq 6449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
212211feq2d 6721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴))
213 raleq 3322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑝 = suc 𝑚 → (∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
214212, 2133anbi13d 1439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
215214rspcev 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
21656, 97, 126, 210, 215syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217 snex 5435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} ∈ V
21832, 217unex 7765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
21922, 23, 218axdc3lem3 10493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220216, 219sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2212203coml 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
2222213exp 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑧𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
223222expd 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (𝐹‘(𝑥𝑚)) → (𝑧𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
22453, 223sylcom 30 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
2252243impd 1348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
226225ex 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚𝐴 → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
227226com23 86 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥:suc 𝑚𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
22849, 227mpdi 45 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229228imp 406 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
230 resundir 6011 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
231 frel 6740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥:suc 𝑚𝐴 → Rel 𝑥)
232 resdm 6043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
233231, 232syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥:suc 𝑚𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
234233adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
23568, 72sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → dom 𝑥 ∈ ω)
23673, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
237 incom 4208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
238237eqeq1i 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
23958, 59fnsn 6623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
240 fnresdisj 6687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
241239, 240ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
242238, 241, 1043bitr3ri 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
243236, 242sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
244235, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245234, 244uneq12d 4168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
246 un0 4393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∪ ∅) = 𝑥
247245, 246eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
248230, 247eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
249248ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2502493adant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
2512503ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252251adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253102uneq2i 4164 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
254 dmun 5920 . . . . . . . . . . . . . . . . . . . . . . . 24 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
255 df-suc 6389 . . . . . . . . . . . . . . . . . . . . . . . 24 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
256253, 254, 2553eqtr4i 2774 . . . . . . . . . . . . . . . . . . . . . . 23 dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
257252, 256jctil 519 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
258 dmeq 5913 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
259258eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
260 reseq1 5990 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
261260eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
262259, 261anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
263262rspcev 3621 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
264229, 257, 263syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω))) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
2652643exp2 1354 . . . . . . . . . . . . . . . . . . . 20 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
266265exlimdv 1932 . . . . . . . . . . . . . . . . . . 19 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
267266adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
26848, 267mpd 15 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
269268com3r 87 . . . . . . . . . . . . . . . 16 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
27034, 269mpan2d 694 . . . . . . . . . . . . . . 15 ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
271270com3r 87 . . . . . . . . . . . . . 14 ((𝑥‘∅) = 𝐶 → ((∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) ∧ 𝑥:suc 𝑚𝐴𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
2722713expd 1353 . . . . . . . . . . . . 13 ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑥:suc 𝑚𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
273272com3r 87 . . . . . . . . . . . 12 (𝑥:suc 𝑚𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
2742733imp 1110 . . . . . . . . . . 11 ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275274com12 32 . . . . . . . . . 10 (𝑚 ∈ ω → ((𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
276275rexlimiv 3147 . . . . . . . . 9 (∃𝑚 ∈ ω (𝑥:suc 𝑚𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
27733, 276sylbi 217 . . . . . . . 8 (𝑥𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
278277impcom 407 . . . . . . 7 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
279 rabn0 4388 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
280278, 279sylibr 234 . . . . . 6 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
28128rabex 5338 . . . . . . . 8 {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
282281elsn 4640 . . . . . . 7 ({𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
283282necon3bbii 2987 . . . . . 6 (¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284280, 283sylibr 234 . . . . 5 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → ¬ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
28531, 284eldifd 3961 . . . 4 ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥𝑆) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
286 axdc3lem4.3 . . . 4 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
287285, 286fmptd 7133 . . 3 (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
28828axdc2 10490 . . 3 ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
28927, 287, 288syl2an 596 . 2 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))))
29022, 23, 286axdc3lem2 10492 . 2 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
291289, 290syl 17 1 ((𝐶𝐴𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1539  wex 1778  wcel 2107  {cab 2713  wne 2939  wral 3060  wrex 3069  {crab 3435  Vcvv 3479  cdif 3947  cun 3948  cin 3949  wss 3950  c0 4332  𝒫 cpw 4599  {csn 4625  cop 4631  cmpt 5224  dom cdm 5684  cres 5686  Rel wrel 5689  Ord word 6382  suc csuc 6385  Fun wfun 6554   Fn wfn 6555  wf 6556  cfv 6560  ωcom 7888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-dc 10487
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-om 7889  df-1o 8507
This theorem is referenced by:  axdc3  10495
  Copyright terms: Public domain W3C validator