Theorem axdc3lem4 9158

Description: Lemma for axdc3 9159. 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 9151 (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 9151 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 9154. See axdc3lem2 9156 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.

Step	Hyp	Ref	Expression
1		peano1 6977	. . . . . 6 ⊢ ∅ ∈ ω
2		eqid 2610	. . . . . . . . . 10 ⊢ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3		fsng 6310	. . . . . . . . . . 11 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
4	1, 3	mpan 702	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
5	2, 4	mpbiri 247	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6		snssi 4280	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴)
7	5, 6	fssd 5970	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8		suc0 5716	. . . . . . . . 9 ⊢ suc ∅ = {∅}
9	8	feq2i 5950	. . . . . . . 8 ⊢ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
10	7, 9	sylibr 223	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11		fvsng 6352	. . . . . . . 8 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
12	1, 11	mpan 702	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13		ral0 4028	. . . . . . . 8 ⊢ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
14	13	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
15	10, 12, 14	3jca 1235	. . . . . 6 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16		suceq 5707	. . . . . . . . 9 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
17	16	feq2d 5944	. . . . . . . 8 ⊢ (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18		raleq 3115	. . . . . . . 8 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
19	17, 18	3anbi13d 1393	. . . . . . 7 ⊢ (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
20	19	rspcev 3282	. . . . . 6 ⊢ ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
21	1, 15, 20	sylancr 694	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22		axdc3lem4.1	. . . . . 6 ⊢ 𝐴 ∈ V
23		axdc3lem4.2	. . . . . 6 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
24		snex 4835	. . . . . 6 ⊢ {⟨∅, 𝐶⟩} ∈ V
25	22, 23, 24	axdc3lem3 9157	. . . . 5 ⊢ ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
26	21, 25	sylibr 223	. . . 4 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
27		ne0i 3880	. . . 4 ⊢ ({⟨∅, 𝐶⟩} ∈ 𝑆 → 𝑆 ≠ ∅)
28	26, 27	syl 17	. . 3 ⊢ (𝐶 ∈ 𝐴 → 𝑆 ≠ ∅)
29		ssrab2 3650	. . . . . . 7 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
30	22, 23	axdc3lem 9155	. . . . . . . 8 ⊢ 𝑆 ∈ V
31	30	elpw2 4755	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆 ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆)
32	29, 31	mpbir 220	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
33	32	a1i 11	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
34		vex 3176	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
35	22, 23, 34	axdc3lem3 9157	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
36		simp2 1055	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → 𝑥:suc 𝑚⟶𝐴)
37		vex 3176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑚 ∈ V
38	37	sucid 5721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑚 ∈ suc 𝑚
39		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑥‘𝑚) ∈ 𝐴)
40	38, 39	mpan2 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥‘𝑚) ∈ 𝐴)
41		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥‘𝑚) ∈ 𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
42	40, 41	sylan2 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
43		eldifn 3695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅})
44		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘(𝑥‘𝑚)) ∈ V
45	44	elsn 4140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) = ∅)
46	45	necon3bbii 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) ≠ ∅)
47		n0 3890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑥‘𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
48	46, 47	bitri 263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
49	43, 48	sylib 207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
50	42, 49	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
51		simp32 1091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → 𝑥:suc 𝑚⟶𝐴)
52		eldifi 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴)
53		elelpwi 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) → 𝑧 ∈ 𝐴)
54	53	expcom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
55	42, 52, 54	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
56		peano2 6978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ ω → suc 𝑚 ∈ ω)
57	56	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → suc 𝑚 ∈ ω)
58	57	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
59		simplr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥:suc 𝑚⟶𝐴)
60	34	dmex 6991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ dom 𝑥 ∈ V
61		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ 𝑧 ∈ V
62		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
63		fsng 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
64	62, 63	mpbiri 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
65	60, 61, 64	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
66		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
67	66	snssd 4281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {𝑧} ⊆ 𝐴)
68		fss 5969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
69	65, 67, 68	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
70		fdm 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → dom 𝑥 = suc 𝑚)
71	56	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
72		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
73	72	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
74	71, 73	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
75		nnord 6965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 ∈ ω → Ord dom 𝑥)
76		ordirr 5658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
77	74, 75, 76	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
78		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
79	78	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
80	77, 79	mtbid 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
81		disjsn 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
82	80, 81	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
83	70, 82	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
84	83	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
85		fun2 5980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑥:suc 𝑚⟶𝐴 ∧ {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴) ∧ (suc 𝑚 ∩ {dom 𝑥}) = ∅) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
86	59, 69, 84, 85	syl21anc 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
87		sneq 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
88	87	uneq2d 3729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
89		df-suc 5646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
90	88, 89	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
91	70, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
92	91	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
93	92	feq2d 5944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
94	86, 93	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
95	94	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ 𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
96	95	adantrd 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
97	96	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
98	97	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
99	98	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
100	99	3imp 1249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
101		ffun 5961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → Fun 𝑥)
102	101	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun 𝑥)
103	60, 61	funsn 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ Fun {⟨dom 𝑥, 𝑧⟩}
104	102, 103	jctir 559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
105	61	dmsnop 5527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
106	105	ineq2i 3773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
107		disjsn 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
108	77, 107	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
109	106, 108	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
110	70, 109	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
111		funun 5846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112	104, 110, 111	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
113		ssun1 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
115		nnord 6965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑚 ∈ ω → Ord 𝑚)
116		0elsuc 6927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (Ord 𝑚 → ∅ ∈ suc 𝑚)
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
118	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ suc 𝑚)
119	70	eleq2d 2673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
120	119	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
121	118, 120	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ dom 𝑥)
122		funssfv 6119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
123	112, 114, 121, 122	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
124	123	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
125	124	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
126	125	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
127	126	biimpar 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
128	127	adantrl 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
129	128	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
130		nfra1 2925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))
131		nfv 1830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑥:suc 𝑚⟶𝐴
132		nfv 1830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑚 ∈ ω
133	130, 131, 132	nf3an 1819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)
134		nfv 1830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐹‘(𝑥‘𝑚))
135		nfv 1830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)
136	133, 134, 135	nf3an 1819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶))
137		simplr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ suc 𝑚)
138		elsuci 5708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ suc 𝑚 → (𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚))
139		rsp 2913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑘 ∈ 𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
140	139	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑘 ∈ 𝑚 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
141	140	ad2ant2lr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
142	141	3adant3 1074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
143	112	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
144	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
145		ordsucelsuc 6914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (Ord 𝑚 → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
146	115, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑚 ∈ ω → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
147	146	biimpa 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → suc 𝑘 ∈ suc 𝑚)
148		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
149	148	biimparc 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
150	147, 70, 149	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom 𝑥)
151		funssfv 6119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
152	143, 144, 150, 151	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
153	152	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
154	112	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
155	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
156		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚))
157	156	biimparc 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
158	70, 157	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
159	158	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
160		funssfv 6119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
161	154, 155, 159, 160	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
162	161	3adant1r 1311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
163	162	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑘)))
164	153, 163	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
165	164	3adant2l 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
166	142, 165	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
167	166	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
168	167	3expib 1260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
169	168	expcom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 ∈ 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
170	112	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
171		ssun2 3739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
173		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
174	173	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
175	174	biimpar 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
176	60	snid 4155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ dom 𝑥 ∈ {dom 𝑥}
177	176, 105	eleqtrri 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
178	175, 177	syl6eqelr 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
179	70, 178	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
180	179	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
181		funssfv 6119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
182	170, 172, 180, 181	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
183	175	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
184	60, 61	fvsn 6351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
185		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
186	184, 185	syl5reqr 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
187	183, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
188	70, 187	syl3an3 1353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
189	182, 188	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
190	189	3expa 1257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
191	190	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
192	161	3adant1l 1310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
193		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑘 = 𝑚 → (𝑥‘𝑘) = (𝑥‘𝑚))
194	193	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (𝑥‘𝑘) = (𝑥‘𝑚))
195	194	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘𝑘) = (𝑥‘𝑚))
196	192, 195	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑚))
197	196	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑚)))
198	191, 197	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
199	198	3adant2l 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
200	199	biimprd 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
201	200	3expib 1260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
202	201	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
203	169, 202	jaoi 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
204	138, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205	204	com3r 85	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
206	137, 205	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207	206	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
208	207	expcom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ suc 𝑚 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
209	208	3impd 1273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ suc 𝑚 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
210	209	impd 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ suc 𝑚 → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
211	210	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
212	211	3adant3 1074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
213	136, 212	ralrimi 2940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
214		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
215	214	feq2d 5944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
216		raleq 3115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → (∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217	215, 216	3anbi13d 1393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
218	217	rspcev 3282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
219	58, 100, 129, 213, 218	syl13anc 1320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220		snex 4835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} ∈ V
221	34, 220	unex 6854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
222	22, 23, 221	axdc3lem3 9157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
223	219, 222	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
224	223	3coml 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
225	224	3exp 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
226	225	expd 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → (𝑧 ∈ 𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
227	55, 226	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
228	227	3impd 1273	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229	228	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚⟶𝐴 → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
230	229	com23 84	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥:suc 𝑚⟶𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
231	51, 230	mpdi 44	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
232	231	imp 444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
233		resundir 5331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
234		frel 5963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥:suc 𝑚⟶𝐴 → Rel 𝑥)
235		resdm 5361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
237	236	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
238	70, 74	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → dom 𝑥 ∈ ω)
239	75, 76	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
240		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
241	240	eqeq1i 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
242	60, 61	fnsn 5860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
243		fnresdisj 5915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
244	242, 243	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245	241, 244, 107	3bitr3ri 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
246	239, 245	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
247	238, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
248	237, 247	uneq12d 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
249		un0 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∪ ∅) = 𝑥
250	248, 249	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
251	233, 250	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252	251	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253	252	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
254	253	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
255	254	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
256	105	uneq2i 3726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
257		dmun 5253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
258		df-suc 5646	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
259	256, 257, 258	3eqtr4i 2642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
260	255, 259	jctil 558	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
261		dmeq 5246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
262	261	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
263		reseq1 5311	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
264	263	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
265	262, 264	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
266	265	rspcev 3282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
267	232, 260, 266	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
268	267	3exp2 1277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
269	268	exlimdv 1848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
270	269	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
271	50, 270	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
272	271	com3r 85	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
273	36, 272	mpan2d 706	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
274	273	com3r 85	. . . . . . . . . . . . . 14 ⊢ ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275	274	3expd 1276	. . . . . . . . . . . . 13 ⊢ ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
276	275	com3r 85	. . . . . . . . . . . 12 ⊢ (𝑥:suc 𝑚⟶𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
277	276	3imp 1249	. . . . . . . . . . 11 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
278	277	com12 32	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
279	278	rexlimiv 3009	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
280	35, 279	sylbi 206	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
281	280	impcom 445	. . . . . . 7 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
282		rabn0 3912	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
283	281, 282	sylibr 223	. . . . . 6 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284	30	rabex 4740	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
285	284	elsn 4140	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
286	285	necon3bbii 2829	. . . . . 6 ⊢ (¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
287	283, 286	sylibr 223	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
288	33, 287	eldifd 3551	. . . 4 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
289		axdc3lem4.3	. . . 4 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
290	288, 289	fmptd 6292	. . 3 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
291	30	axdc2 9154	. . 3 ⊢ ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
292	28, 290, 291	syl2an 493	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
293	22, 23, 289	axdc3lem2 9156	. 2 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
294	292, 293	syl 17	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ⟨cop 4131   ↦ cmpt 4643  dom cdm 5038   ↾ cres 5040  Rel wrel 5043  Ord word 5639  suc csuc 5642  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  ωcom 6957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-dc 9151

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-1o 7447

This theorem is referenced by:  axdc3  9159