This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axdc3lem4

Description: Lemma for axdc3 . We have constructed a "candidate set" S , which consists of all finite sequences s that satisfy our property of interest, namely s ( x + 1 ) e. F ( s ( x ) ) on its domain, but with the added constraint that s ( 0 ) = C . These sets are possible "initial segments" of theinfinite sequence satisfying these constraints, but we can leverage the standard ax-dc (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely ( hn ) : m --> A (for some integer m ). 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 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 S is nonempty, and that G always maps to a nonempty subset of S , so that we can apply axdc2 . See axdc3lem2 for the rest of the proof. (Contributed by Mario Carneiro, 27-Jan-2013)

Ref Expression
Hypotheses axdc3lem4.1 ⊢ 𝐴 ∈ V
axdc3lem4.2 ⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
axdc3lem4.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } )
Assertion axdc3lem4 ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc3lem4.1 ⊢ 𝐴 ∈ V
2 axdc3lem4.2 ⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
3 axdc3lem4.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } )
4 peano1 ⊢ ∅ ∈ ω
5 eqid ⊢ { ⟨ ∅ , 𝐶 ⟩ } = { ⟨ ∅ , 𝐶 ⟩ }
6 fsng ⊢ ( ( ∅ ∈ ω ∧ 𝐶 ∈ 𝐴 ) → ( { ⟨ ∅ , 𝐶 ⟩ } : { ∅ } ⟶ { 𝐶 } ↔ { ⟨ ∅ , 𝐶 ⟩ } = { ⟨ ∅ , 𝐶 ⟩ } ) )
7 4 6 mpan ⊢ ( 𝐶 ∈ 𝐴 → ( { ⟨ ∅ , 𝐶 ⟩ } : { ∅ } ⟶ { 𝐶 } ↔ { ⟨ ∅ , 𝐶 ⟩ } = { ⟨ ∅ , 𝐶 ⟩ } ) )
8 5 7 mpbiri ⊢ ( 𝐶 ∈ 𝐴 → { ⟨ ∅ , 𝐶 ⟩ } : { ∅ } ⟶ { 𝐶 } )
9 snssi ⊢ ( 𝐶 ∈ 𝐴 → { 𝐶 } ⊆ 𝐴 )
10 8 9 fssd ⊢ ( 𝐶 ∈ 𝐴 → { ⟨ ∅ , 𝐶 ⟩ } : { ∅ } ⟶ 𝐴 )
11 suc0 ⊢ suc ∅ = { ∅ }
12 11 feq2i ⊢ ( { ⟨ ∅ , 𝐶 ⟩ } : suc ∅ ⟶ 𝐴 ↔ { ⟨ ∅ , 𝐶 ⟩ } : { ∅ } ⟶ 𝐴 )
13 10 12 sylibr ⊢ ( 𝐶 ∈ 𝐴 → { ⟨ ∅ , 𝐶 ⟩ } : suc ∅ ⟶ 𝐴 )
14 fvsng ⊢ ( ( ∅ ∈ ω ∧ 𝐶 ∈ 𝐴 ) → ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 )
15 4 14 mpan ⊢ ( 𝐶 ∈ 𝐴 → ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 )
16 ral0 ⊢ ∀ 𝑘 ∈ ∅ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) )
17 16 a1i ⊢ ( 𝐶 ∈ 𝐴 → ∀ 𝑘 ∈ ∅ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) )
18 13 15 17 3jca ⊢ ( 𝐶 ∈ 𝐴 → ( { ⟨ ∅ , 𝐶 ⟩ } : suc ∅ ⟶ 𝐴 ∧ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ∅ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) )
19 suceq ⊢ ( 𝑚 = ∅ → suc 𝑚 = suc ∅ )
20 19 feq2d ⊢ ( 𝑚 = ∅ → ( { ⟨ ∅ , 𝐶 ⟩ } : suc 𝑚 ⟶ 𝐴 ↔ { ⟨ ∅ , 𝐶 ⟩ } : suc ∅ ⟶ 𝐴 ) )
21 raleq ⊢ ( 𝑚 = ∅ → ( ∀ 𝑘 ∈ 𝑚 ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ ∅ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) )
22 20 21 3anbi13d ⊢ ( 𝑚 = ∅ → ( ( { ⟨ ∅ , 𝐶 ⟩ } : suc 𝑚 ⟶ 𝐴 ∧ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) ↔ ( { ⟨ ∅ , 𝐶 ⟩ } : suc ∅ ⟶ 𝐴 ∧ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ∅ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) ) )
23 22 rspcev ⊢ ( ( ∅ ∈ ω ∧ ( { ⟨ ∅ , 𝐶 ⟩ } : suc ∅ ⟶ 𝐴 ∧ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ∅ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) ) → ∃ 𝑚 ∈ ω ( { ⟨ ∅ , 𝐶 ⟩ } : suc 𝑚 ⟶ 𝐴 ∧ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) )
24 4 18 23 sylancr ⊢ ( 𝐶 ∈ 𝐴 → ∃ 𝑚 ∈ ω ( { ⟨ ∅ , 𝐶 ⟩ } : suc 𝑚 ⟶ 𝐴 ∧ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) )
25 snex ⊢ { ⟨ ∅ , 𝐶 ⟩ } ∈ V
26 1 2 25 axdc3lem3 ⊢ ( { ⟨ ∅ , 𝐶 ⟩ } ∈ 𝑆 ↔ ∃ 𝑚 ∈ ω ( { ⟨ ∅ , 𝐶 ⟩ } : suc 𝑚 ⟶ 𝐴 ∧ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( { ⟨ ∅ , 𝐶 ⟩ } ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( { ⟨ ∅ , 𝐶 ⟩ } ‘ 𝑘 ) ) ) )
27 24 26 sylibr ⊢ ( 𝐶 ∈ 𝐴 → { ⟨ ∅ , 𝐶 ⟩ } ∈ 𝑆 )
28 27 ne0d ⊢ ( 𝐶 ∈ 𝐴 → 𝑆 ≠ ∅ )
29 1 2 axdc3lem ⊢ 𝑆 ∈ V
30 ssrab2 ⊢ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ⊆ 𝑆
31 29 30 elpwi2 ⊢ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ∈ 𝒫 𝑆
32 31 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝑆 ) → { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ∈ 𝒫 𝑆 )
33 vex ⊢ 𝑥 ∈ V
34 1 2 33 axdc3lem3 ⊢ ( 𝑥 ∈ 𝑆 ↔ ∃ 𝑚 ∈ ω ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) )
35 simp2 ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → 𝑥 : suc 𝑚 ⟶ 𝐴 )
36 vex ⊢ 𝑚 ∈ V
37 36 sucid ⊢ 𝑚 ∈ suc 𝑚
38 ffvelcdm ⊢ ( ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ suc 𝑚 ) → ( 𝑥 ‘ 𝑚 ) ∈ 𝐴 )
39 37 38 mpan2 ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( 𝑥 ‘ 𝑚 ) ∈ 𝐴 )
40 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ ( 𝑥 ‘ 𝑚 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
41 39 40 sylan2 ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
42 eldifn ⊢ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ¬ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ { ∅ } )
43 fvex ⊢ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ V
44 43 elsn ⊢ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ { ∅ } ↔ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) = ∅ )
45 44 necon3bbii ⊢ ( ¬ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ { ∅ } ↔ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ≠ ∅ )
46 n0 ⊢ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) )
47 45 46 bitri ⊢ ( ¬ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ { ∅ } ↔ ∃ 𝑧 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) )
48 42 47 sylib ⊢ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑧 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) )
49 41 48 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ∃ 𝑧 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) )
50 simp32 ⊢ ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) → 𝑥 : suc 𝑚 ⟶ 𝐴 )
51 eldifi ⊢ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ 𝒫 𝐴 )
52 elelpwi ⊢ ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ 𝒫 𝐴 ) → 𝑧 ∈ 𝐴 )
53 52 expcom ⊢ ( ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∈ 𝒫 𝐴 → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → 𝑧 ∈ 𝐴 ) )
54 41 51 53 3syl ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → 𝑧 ∈ 𝐴 ) )
55 peano2 ⊢ ( 𝑚 ∈ ω → suc 𝑚 ∈ ω )
56 55 3ad2ant3 ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → suc 𝑚 ∈ ω )
57 56 3ad2ant1 ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → suc 𝑚 ∈ ω )
58 simplr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 : suc 𝑚 ⟶ 𝐴 )
59 33 dmex ⊢ dom 𝑥 ∈ V
60 vex ⊢ 𝑧 ∈ V
61 eqid ⊢ { ⟨ dom 𝑥 , 𝑧 ⟩ } = { ⟨ dom 𝑥 , 𝑧 ⟩ }
62 fsng ⊢ ( ( dom 𝑥 ∈ V ∧ 𝑧 ∈ V ) → ( { ⟨ dom 𝑥 , 𝑧 ⟩ } : { dom 𝑥 } ⟶ { 𝑧 } ↔ { ⟨ dom 𝑥 , 𝑧 ⟩ } = { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
63 61 62 mpbiri ⊢ ( ( dom 𝑥 ∈ V ∧ 𝑧 ∈ V ) → { ⟨ dom 𝑥 , 𝑧 ⟩ } : { dom 𝑥 } ⟶ { 𝑧 } )
64 59 60 63 mp2an ⊢ { ⟨ dom 𝑥 , 𝑧 ⟩ } : { dom 𝑥 } ⟶ { 𝑧 }
65 simpr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
66 65 snssd ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → { 𝑧 } ⊆ 𝐴 )
67 fss ⊢ ( ( { ⟨ dom 𝑥 , 𝑧 ⟩ } : { dom 𝑥 } ⟶ { 𝑧 } ∧ { 𝑧 } ⊆ 𝐴 ) → { ⟨ dom 𝑥 , 𝑧 ⟩ } : { dom 𝑥 } ⟶ 𝐴 )
68 64 66 67 sylancr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → { ⟨ dom 𝑥 , 𝑧 ⟩ } : { dom 𝑥 } ⟶ 𝐴 )
69 fdm ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → dom 𝑥 = suc 𝑚 )
70 55 adantr ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → suc 𝑚 ∈ ω )
71 eleq1 ⊢ ( dom 𝑥 = suc 𝑚 → ( dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω ) )
72 71 adantl ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ( dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω ) )
73 70 72 mpbird ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → dom 𝑥 ∈ ω )
74 nnord ⊢ ( dom 𝑥 ∈ ω → Ord dom 𝑥 )
75 ordirr ⊢ ( Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥 )
76 73 74 75 3syl ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ¬ dom 𝑥 ∈ dom 𝑥 )
77 eleq2 ⊢ ( dom 𝑥 = suc 𝑚 → ( dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚 ) )
78 77 adantl ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ( dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚 ) )
79 76 78 mtbid ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ¬ dom 𝑥 ∈ suc 𝑚 )
80 disjsn ⊢ ( ( suc 𝑚 ∩ { dom 𝑥 } ) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚 )
81 79 80 sylibr ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ( suc 𝑚 ∩ { dom 𝑥 } ) = ∅ )
82 69 81 sylan2 ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( suc 𝑚 ∩ { dom 𝑥 } ) = ∅ )
83 82 adantr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( suc 𝑚 ∩ { dom 𝑥 } ) = ∅ )
84 58 68 83 fun2d ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : ( suc 𝑚 ∪ { dom 𝑥 } ) ⟶ 𝐴 )
85 sneq ⊢ ( dom 𝑥 = suc 𝑚 → { dom 𝑥 } = { suc 𝑚 } )
86 85 uneq2d ⊢ ( dom 𝑥 = suc 𝑚 → ( suc 𝑚 ∪ { dom 𝑥 } ) = ( suc 𝑚 ∪ { suc 𝑚 } ) )
87 df-suc ⊢ suc suc 𝑚 = ( suc 𝑚 ∪ { suc 𝑚 } )
88 86 87 eqtr4di ⊢ ( dom 𝑥 = suc 𝑚 → ( suc 𝑚 ∪ { dom 𝑥 } ) = suc suc 𝑚 )
89 69 88 syl ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( suc 𝑚 ∪ { dom 𝑥 } ) = suc suc 𝑚 )
90 89 ad2antlr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( suc 𝑚 ∪ { dom 𝑥 } ) = suc suc 𝑚 )
91 90 feq2d ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : ( suc 𝑚 ∪ { dom 𝑥 } ) ⟶ 𝐴 ↔ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ) )
92 84 91 mpbid ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 )
93 92 ex ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ 𝐴 → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ) )
94 93 adantrd ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ) )
95 94 a1d ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ) ) )
96 95 ancoms ⊢ ( ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ) ) )
97 96 3adant1 ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ) ) )
98 97 3imp ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 )
99 ffun ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → Fun 𝑥 )
100 99 adantl ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → Fun 𝑥 )
101 59 60 funsn ⊢ Fun { ⟨ dom 𝑥 , 𝑧 ⟩ }
102 100 101 jctir ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( Fun 𝑥 ∧ Fun { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
103 60 dmsnop ⊢ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } = { dom 𝑥 }
104 103 ineq2i ⊢ ( dom 𝑥 ∩ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = ( dom 𝑥 ∩ { dom 𝑥 } )
105 disjsn ⊢ ( ( dom 𝑥 ∩ { dom 𝑥 } ) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥 )
106 76 105 sylibr ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ( dom 𝑥 ∩ { dom 𝑥 } ) = ∅ )
107 104 106 eqtrid ⊢ ( ( 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ( dom 𝑥 ∩ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = ∅ )
108 69 107 sylan2 ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( dom 𝑥 ∩ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = ∅ )
109 funun ⊢ ( ( ( Fun 𝑥 ∧ Fun { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ ( dom 𝑥 ∩ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = ∅ ) → Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
110 102 108 109 syl2anc ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
111 ssun1 ⊢ 𝑥 ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } )
112 111 a1i ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → 𝑥 ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
113 nnord ⊢ ( 𝑚 ∈ ω → Ord 𝑚 )
114 0elsuc ⊢ ( Ord 𝑚 → ∅ ∈ suc 𝑚 )
115 113 114 syl ⊢ ( 𝑚 ∈ ω → ∅ ∈ suc 𝑚 )
116 115 adantr ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ∅ ∈ suc 𝑚 )
117 69 eleq2d ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( ∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚 ) )
118 117 adantl ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚 ) )
119 116 118 mpbird ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ∅ ∈ dom 𝑥 )
120 funssfv ⊢ ( ( Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ 𝑥 ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ ∅ ∈ dom 𝑥 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = ( 𝑥 ‘ ∅ ) )
121 110 112 119 120 syl3anc ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = ( 𝑥 ‘ ∅ ) )
122 121 eqeq1d ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ↔ ( 𝑥 ‘ ∅ ) = 𝐶 ) )
123 122 ancoms ⊢ ( ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ↔ ( 𝑥 ‘ ∅ ) = 𝐶 ) )
124 123 3adant1 ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ↔ ( 𝑥 ‘ ∅ ) = 𝐶 ) )
125 124 biimpar ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 )
126 125 adantrl ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 )
127 126 3adant2 ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 )
128 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) )
129 nfv ⊢ Ⅎ 𝑘 𝑥 : suc 𝑚 ⟶ 𝐴
130 nfv ⊢ Ⅎ 𝑘 𝑚 ∈ ω
131 128 129 130 nf3an ⊢ Ⅎ 𝑘 ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω )
132 nfv ⊢ Ⅎ 𝑘 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) )
133 nfv ⊢ Ⅎ 𝑘 ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 )
134 131 132 133 nf3an ⊢ Ⅎ 𝑘 ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) )
135 simplr ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → 𝑘 ∈ suc 𝑚 )
136 elsuci ⊢ ( 𝑘 ∈ suc 𝑚 → ( 𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚 ) )
137 rsp ⊢ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) → ( 𝑘 ∈ 𝑚 → ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) )
138 137 impcom ⊢ ( ( 𝑘 ∈ 𝑚 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) → ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) )
139 138 ad2ant2lr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ) → ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) )
140 139 3adant3 ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) )
141 110 adantlr ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
142 111 a1i ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → 𝑥 ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
143 ordsucelsuc ⊢ ( Ord 𝑚 → ( 𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚 ) )
144 113 143 syl ⊢ ( 𝑚 ∈ ω → ( 𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚 ) )
145 144 biimpa ⊢ ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) → suc 𝑘 ∈ suc 𝑚 )
146 eleq2 ⊢ ( dom 𝑥 = suc 𝑚 → ( suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚 ) )
147 146 biimparc ⊢ ( ( suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚 ) → suc 𝑘 ∈ dom 𝑥 )
148 145 69 147 syl2an ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → suc 𝑘 ∈ dom 𝑥 )
149 funssfv ⊢ ( ( Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ 𝑥 ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ suc 𝑘 ∈ dom 𝑥 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = ( 𝑥 ‘ suc 𝑘 ) )
150 141 142 148 149 syl3anc ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = ( 𝑥 ‘ suc 𝑘 ) )
151 150 3adant2 ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = ( 𝑥 ‘ suc 𝑘 ) )
152 110 3adant2 ⊢ ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
153 111 a1i ⊢ ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → 𝑥 ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
154 eleq2 ⊢ ( dom 𝑥 = suc 𝑚 → ( 𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚 ) )
155 154 biimparc ⊢ ( ( 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚 ) → 𝑘 ∈ dom 𝑥 )
156 69 155 sylan2 ⊢ ( ( 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → 𝑘 ∈ dom 𝑥 )
157 156 3adant1 ⊢ ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → 𝑘 ∈ dom 𝑥 )
158 funssfv ⊢ ( ( Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ 𝑥 ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ 𝑘 ∈ dom 𝑥 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) = ( 𝑥 ‘ 𝑘 ) )
159 152 153 157 158 syl3anc ⊢ ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) = ( 𝑥 ‘ 𝑘 ) )
160 159 3adant1r ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) = ( 𝑥 ‘ 𝑘 ) )
161 160 fveq2d ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) )
162 151 161 eleq12d ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ↔ ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) )
163 162 3adant2l ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ↔ ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) )
164 140 163 mpbird ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) )
165 164 a1d ⊢ ( ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
166 165 3expib ⊢ ( ( 𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚 ) → ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) )
167 166 expcom ⊢ ( 𝑘 ∈ 𝑚 → ( 𝑚 ∈ ω → ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) ) )
168 110 3adant1 ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
169 ssun2 ⊢ { ⟨ dom 𝑥 , 𝑧 ⟩ } ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } )
170 169 a1i ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → { ⟨ dom 𝑥 , 𝑧 ⟩ } ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
171 suceq ⊢ ( 𝑘 = 𝑚 → suc 𝑘 = suc 𝑚 )
172 171 eqeq2d ⊢ ( 𝑘 = 𝑚 → ( dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚 ) )
173 172 biimpar ⊢ ( ( 𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚 ) → dom 𝑥 = suc 𝑘 )
174 59 snid ⊢ dom 𝑥 ∈ { dom 𝑥 }
175 174 103 eleqtrri ⊢ dom 𝑥 ∈ dom { ⟨ dom 𝑥 , 𝑧 ⟩ }
176 173 175 eqeltrrdi ⊢ ( ( 𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚 ) → suc 𝑘 ∈ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } )
177 69 176 sylan2 ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → suc 𝑘 ∈ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } )
178 177 3adant2 ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → suc 𝑘 ∈ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } )
179 funssfv ⊢ ( ( Fun ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ { ⟨ dom 𝑥 , 𝑧 ⟩ } ⊆ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∧ suc 𝑘 ∈ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ suc 𝑘 ) )
180 168 170 178 179 syl3anc ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ suc 𝑘 ) )
181 173 3adant2 ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → dom 𝑥 = suc 𝑘 )
182 fveq2 ⊢ ( dom 𝑥 = suc 𝑘 → ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ dom 𝑥 ) = ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ suc 𝑘 ) )
183 59 60 fvsn ⊢ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ dom 𝑥 ) = 𝑧
184 182 183 eqtr3di ⊢ ( dom 𝑥 = suc 𝑘 → ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ suc 𝑘 ) = 𝑧 )
185 181 184 syl ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚 ) → ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ suc 𝑘 ) = 𝑧 )
186 69 185 syl3an3 ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ‘ suc 𝑘 ) = 𝑧 )
187 180 186 eqtrd ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = 𝑧 )
188 187 3expa ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = 𝑧 )
189 188 3adant2 ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) = 𝑧 )
190 159 3adant1l ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) = ( 𝑥 ‘ 𝑘 ) )
191 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑥 ‘ 𝑘 ) = ( 𝑥 ‘ 𝑚 ) )
192 191 adantr ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) → ( 𝑥 ‘ 𝑘 ) = ( 𝑥 ‘ 𝑚 ) )
193 192 3ad2ant1 ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑥 ‘ 𝑘 ) = ( 𝑥 ‘ 𝑚 ) )
194 190 193 eqtrd ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) = ( 𝑥 ‘ 𝑚 ) )
195 194 fveq2d ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) )
196 189 195 eleq12d ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ) )
197 196 3adant2l ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ↔ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ) )
198 197 biimprd ⊢ ( ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
199 198 3expib ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑚 ∈ ω ) → ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) )
200 199 ex ⊢ ( 𝑘 = 𝑚 → ( 𝑚 ∈ ω → ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) ) )
201 167 200 jaoi ⊢ ( ( 𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚 ) → ( 𝑚 ∈ ω → ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) ) )
202 136 201 syl ⊢ ( 𝑘 ∈ suc 𝑚 → ( 𝑚 ∈ ω → ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) ) )
203 202 com3r ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑘 ∈ suc 𝑚 → ( 𝑚 ∈ ω → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) ) )
204 135 203 mpd ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑚 ∈ ω → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) )
205 204 ex ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑘 ∈ suc 𝑚 ) → ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( 𝑚 ∈ ω → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) ) )
206 205 expcom ⊢ ( 𝑘 ∈ suc 𝑚 → ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) → ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( 𝑚 ∈ ω → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) ) ) )
207 206 3impd ⊢ ( 𝑘 ∈ suc 𝑚 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) )
208 207 impd ⊢ ( 𝑘 ∈ suc 𝑚 → ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
209 208 com12 ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ) → ( 𝑘 ∈ suc 𝑚 → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
210 209 3adant3 ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → ( 𝑘 ∈ suc 𝑚 → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
211 134 210 ralrimi ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → ∀ 𝑘 ∈ suc 𝑚 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) )
212 suceq ⊢ ( 𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚 )
213 212 feq2d ⊢ ( 𝑝 = suc 𝑚 → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc 𝑝 ⟶ 𝐴 ↔ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ) )
214 raleq ⊢ ( 𝑝 = suc 𝑚 → ( ∀ 𝑘 ∈ 𝑝 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ suc 𝑚 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
215 213 214 3anbi13d ⊢ ( 𝑝 = suc 𝑚 → ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc 𝑝 ⟶ 𝐴 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑝 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ↔ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ suc 𝑚 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) )
216 215 rspcev ⊢ ( ( suc 𝑚 ∈ ω ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc suc 𝑚 ⟶ 𝐴 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ suc 𝑚 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) ) → ∃ 𝑝 ∈ ω ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc 𝑝 ⟶ 𝐴 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑝 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
217 57 98 127 211 216 syl13anc ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → ∃ 𝑝 ∈ ω ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc 𝑝 ⟶ 𝐴 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑝 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
218 snex ⊢ { ⟨ dom 𝑥 , 𝑧 ⟩ } ∈ V
219 33 218 unex ⊢ ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ V
220 1 2 219 axdc3lem3 ⊢ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ↔ ∃ 𝑝 ∈ ω ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) : suc 𝑝 ⟶ 𝐴 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑝 ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ‘ 𝑘 ) ) ) )
221 217 220 sylibr ⊢ ( ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ∧ 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 )
222 221 3coml ⊢ ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 )
223 222 3exp ⊢ ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ) → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ) ) )
224 223 expd ⊢ ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ) ) ) )
225 54 224 sylcom ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ) ) ) )
226 225 3impd ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ) )
227 226 ex ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ) ) )
228 227 com23 ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) → ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ) ) )
229 50 228 mpdi ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ) )
230 229 imp ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) ) → ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 )
231 resundir ⊢ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = ( ( 𝑥 ↾ dom 𝑥 ) ∪ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) )
232 frel ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → Rel 𝑥 )
233 resdm ⊢ ( Rel 𝑥 → ( 𝑥 ↾ dom 𝑥 ) = 𝑥 )
234 232 233 syl ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( 𝑥 ↾ dom 𝑥 ) = 𝑥 )
235 234 adantl ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( 𝑥 ↾ dom 𝑥 ) = 𝑥 )
236 69 73 sylan2 ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → dom 𝑥 ∈ ω )
237 74 75 syl ⊢ ( dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥 )
238 incom ⊢ ( { dom 𝑥 } ∩ dom 𝑥 ) = ( dom 𝑥 ∩ { dom 𝑥 } )
239 238 eqeq1i ⊢ ( ( { dom 𝑥 } ∩ dom 𝑥 ) = ∅ ↔ ( dom 𝑥 ∩ { dom 𝑥 } ) = ∅ )
240 59 60 fnsn ⊢ { ⟨ dom 𝑥 , 𝑧 ⟩ } Fn { dom 𝑥 }
241 fnresdisj ⊢ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } Fn { dom 𝑥 } → ( ( { dom 𝑥 } ∩ dom 𝑥 ) = ∅ ↔ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) = ∅ ) )
242 240 241 ax-mp ⊢ ( ( { dom 𝑥 } ∩ dom 𝑥 ) = ∅ ↔ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) = ∅ )
243 239 242 105 3bitr3ri ⊢ ( ¬ dom 𝑥 ∈ dom 𝑥 ↔ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) = ∅ )
244 237 243 sylib ⊢ ( dom 𝑥 ∈ ω → ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) = ∅ )
245 236 244 syl ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) = ∅ )
246 235 245 uneq12d ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ↾ dom 𝑥 ) ∪ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) ) = ( 𝑥 ∪ ∅ ) )
247 un0 ⊢ ( 𝑥 ∪ ∅ ) = 𝑥
248 246 247 eqtrdi ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ↾ dom 𝑥 ) ∪ ( { ⟨ dom 𝑥 , 𝑧 ⟩ } ↾ dom 𝑥 ) ) = 𝑥 )
249 231 248 eqtrid ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 )
250 249 ancoms ⊢ ( ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 )
251 250 3adant1 ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 )
252 251 3ad2ant3 ⊢ ( ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 )
253 252 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) ) → ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 )
254 103 uneq2i ⊢ ( dom 𝑥 ∪ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = ( dom 𝑥 ∪ { dom 𝑥 } )
255 dmun ⊢ dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = ( dom 𝑥 ∪ dom { ⟨ dom 𝑥 , 𝑧 ⟩ } )
256 df-suc ⊢ suc dom 𝑥 = ( dom 𝑥 ∪ { dom 𝑥 } )
257 254 255 256 3eqtr4i ⊢ dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = suc dom 𝑥
258 253 257 jctil ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) ) → ( dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = suc dom 𝑥 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 ) )
259 dmeq ⊢ ( 𝑦 = ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) → dom 𝑦 = dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) )
260 259 eqeq1d ⊢ ( 𝑦 = ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) → ( dom 𝑦 = suc dom 𝑥 ↔ dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = suc dom 𝑥 ) )
261 reseq1 ⊢ ( 𝑦 = ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) → ( 𝑦 ↾ dom 𝑥 ) = ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) )
262 261 eqeq1d ⊢ ( 𝑦 = ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) → ( ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ↔ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 ) )
263 260 262 anbi12d ⊢ ( 𝑦 = ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) → ( ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ↔ ( dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = suc dom 𝑥 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 ) ) )
264 263 rspcev ⊢ ( ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ∈ 𝑆 ∧ ( dom ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) = suc dom 𝑥 ∧ ( ( 𝑥 ∪ { ⟨ dom 𝑥 , 𝑧 ⟩ } ) ↾ dom 𝑥 ) = 𝑥 ) ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) )
265 230 258 264 syl2anc ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) ) ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) )
266 265 3exp2 ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) ) )
267 266 exlimdv ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ∃ 𝑧 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) ) )
268 267 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ∃ 𝑧 𝑧 ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑚 ) ) → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) ) )
269 49 268 mpd ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) )
270 269 com3r ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ) → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) )
271 35 270 mpan2d ⊢ ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) )
272 271 com3r ⊢ ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ∧ 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ 𝑚 ∈ ω ) → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) )
273 272 3expd ⊢ ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) → ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( 𝑚 ∈ ω → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) ) ) )
274 273 com3r ⊢ ( 𝑥 : suc 𝑚 ⟶ 𝐴 → ( ( 𝑥 ‘ ∅ ) = 𝐶 → ( ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) → ( 𝑚 ∈ ω → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) ) ) )
275 274 3imp ⊢ ( ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) )
276 275 com12 ⊢ ( 𝑚 ∈ ω → ( ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) ) )
277 276 rexlimiv ⊢ ( ∃ 𝑚 ∈ ω ( 𝑥 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝑥 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝑥 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑥 ‘ 𝑘 ) ) ) → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) )
278 34 277 sylbi ⊢ ( 𝑥 ∈ 𝑆 → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ) )
279 278 impcom ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) )
280 rabn0 ⊢ ( { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝑆 ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) )
281 279 280 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝑆 ) → { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ≠ ∅ )
282 29 rabex ⊢ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ∈ V
283 282 elsn ⊢ ( { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ∈ { ∅ } ↔ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } = ∅ )
284 283 necon3bbii ⊢ ( ¬ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ∈ { ∅ } ↔ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ≠ ∅ )
285 281 284 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝑆 ) → ¬ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ∈ { ∅ } )
286 32 285 eldifd ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝑆 ) → { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ∈ ( 𝒫 𝑆 ∖ { ∅ } ) )
287 286 3 fmptd ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝐺 : 𝑆 ⟶ ( 𝒫 𝑆 ∖ { ∅ } ) )
288 29 axdc2 ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝐺 : 𝑆 ⟶ ( 𝒫 𝑆 ∖ { ∅ } ) ) → ∃ ℎ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) )
289 28 287 288 syl2an ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ ℎ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) )
290 1 2 3 axdc3lem2 ⊢ ( ∃ ℎ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
291 289 290 syl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )