Theorem axdc3lem4 10450

Description: Lemma for axdc3 10451. 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 10443 (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 10443 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 10446. See axdc3lem2 10448 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 7881	. . . . . 6 ⊢ ∅ ∈ ω
2		eqid 2730	. . . . . . . . . 10 ⊢ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3		fsng 7136	. . . . . . . . . . 11 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
4	1, 3	mpan 686	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
5	2, 4	mpbiri 257	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6		snssi 4810	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴)
7	5, 6	fssd 6734	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8		suc0 6438	. . . . . . . . 9 ⊢ suc ∅ = {∅}
9	8	feq2i 6708	. . . . . . . 8 ⊢ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
10	7, 9	sylibr 233	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11		fvsng 7179	. . . . . . . 8 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
12	1, 11	mpan 686	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13		ral0 4511	. . . . . . . 8 ⊢ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
14	13	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
15	10, 12, 14	3jca 1126	. . . . . 6 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16		suceq 6429	. . . . . . . . 9 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
17	16	feq2d 6702	. . . . . . . 8 ⊢ (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18		raleq 3320	. . . . . . . 8 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
19	17, 18	3anbi13d 1436	. . . . . . 7 ⊢ (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
20	19	rspcev 3611	. . . . . 6 ⊢ ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
21	1, 15, 20	sylancr 585	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22		axdc3lem4.1	. . . . . 6 ⊢ 𝐴 ∈ V
23		axdc3lem4.2	. . . . . 6 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
24		snex 5430	. . . . . 6 ⊢ {⟨∅, 𝐶⟩} ∈ V
25	22, 23, 24	axdc3lem3 10449	. . . . 5 ⊢ ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
26	21, 25	sylibr 233	. . . 4 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
27	26	ne0d 4334	. . 3 ⊢ (𝐶 ∈ 𝐴 → 𝑆 ≠ ∅)
28	22, 23	axdc3lem 10447	. . . . . . 7 ⊢ 𝑆 ∈ V
29		ssrab2 4076	. . . . . . 7 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
30	28, 29	elpwi2 5345	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
31	30	a1i 11	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
32		vex 3476	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
33	22, 23, 32	axdc3lem3 10449	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
34		simp2 1135	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → 𝑥:suc 𝑚⟶𝐴)
35		vex 3476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑚 ∈ V
36	35	sucid 6445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑚 ∈ suc 𝑚
37		ffvelcdm 7082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑥‘𝑚) ∈ 𝐴)
38	36, 37	mpan2 687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥‘𝑚) ∈ 𝐴)
39		ffvelcdm 7082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥‘𝑚) ∈ 𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
40	38, 39	sylan2 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
41		eldifn 4126	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅})
42		fvex 6903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘(𝑥‘𝑚)) ∈ V
43	42	elsn 4642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) = ∅)
44	43	necon3bbii 2986	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) ≠ ∅)
45		n0 4345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑥‘𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
46	44, 45	bitri 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
47	41, 46	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
48	40, 47	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
49		simp32 1208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → 𝑥:suc 𝑚⟶𝐴)
50		eldifi 4125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴)
51		elelpwi 4611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) → 𝑧 ∈ 𝐴)
52	51	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
53	40, 50, 52	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
54		peano2 7883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ ω → suc 𝑚 ∈ ω)
55	54	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → suc 𝑚 ∈ ω)
56	55	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
57		simplr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥:suc 𝑚⟶𝐴)
58	32	dmex 7904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ dom 𝑥 ∈ V
59		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ 𝑧 ∈ V
60		eqid 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
61		fsng 7136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
62	60, 61	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
63	58, 59, 62	mp2an 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
64		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
65	64	snssd 4811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {𝑧} ⊆ 𝐴)
66		fss 6733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
67	63, 65, 66	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
68		fdm 6725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → dom 𝑥 = suc 𝑚)
69	54	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
70		eleq1 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
71	70	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
72	69, 71	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
73		nnord 7865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 ∈ ω → Ord dom 𝑥)
74		ordirr 6381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
75	72, 73, 74	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
76		eleq2 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
77	76	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
78	75, 77	mtbid 323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
79		disjsn 4714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
80	78, 79	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
81	68, 80	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
82	81	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
83	57, 67, 82	fun2d 6754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
84		sneq 4637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
85	84	uneq2d 4162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
86		df-suc 6369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
87	85, 86	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
88	68, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
89	88	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
90	89	feq2d 6702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
91	83, 90	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
92	91	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ 𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
93	92	adantrd 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
94	93	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
95	94	ancoms 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
96	95	3adant1 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
97	96	3imp 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
98		ffun 6719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → Fun 𝑥)
99	98	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun 𝑥)
100	58, 59	funsn 6600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ Fun {⟨dom 𝑥, 𝑧⟩}
101	99, 100	jctir 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
102	59	dmsnop 6214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
103	102	ineq2i 4208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
104		disjsn 4714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
105	75, 104	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
106	103, 105	eqtrid 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
107	68, 106	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
108		funun 6593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
109	101, 107, 108	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
110		ssun1 4171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
111	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112		nnord 7865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑚 ∈ ω → Ord 𝑚)
113		0elsuc 7825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (Ord 𝑚 → ∅ ∈ suc 𝑚)
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
115	114	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ suc 𝑚)
116	68	eleq2d 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
117	116	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
118	115, 117	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ dom 𝑥)
119		funssfv 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
120	109, 111, 118, 119	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
121	120	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
122	121	ancoms 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
123	122	3adant1 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
124	123	biimpar 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
125	124	adantrl 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
126	125	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
127		nfra1 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))
128		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑥:suc 𝑚⟶𝐴
129		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑚 ∈ ω
130	127, 128, 129	nf3an 1902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)
131		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐹‘(𝑥‘𝑚))
132		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)
133	130, 131, 132	nf3an 1902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶))
134		simplr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ suc 𝑚)
135		elsuci 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ suc 𝑚 → (𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚))
136		rsp 3242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑘 ∈ 𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
137	136	impcom 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑘 ∈ 𝑚 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
138	137	ad2ant2lr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
139	138	3adant3 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
140	109	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
141	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
142		ordsucelsuc 7812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (Ord 𝑚 → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
143	112, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑚 ∈ ω → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
144	143	biimpa 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → suc 𝑘 ∈ suc 𝑚)
145		eleq2 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
146	145	biimparc 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
147	144, 68, 146	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom 𝑥)
148		funssfv 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
149	140, 141, 147, 148	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
150	149	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
151	109	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
152	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
153		eleq2 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚))
154	153	biimparc 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
155	68, 154	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
156	155	3adant1 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
157		funssfv 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
158	151, 152, 156, 157	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
159	158	3adant1r 1175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
160	159	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑘)))
161	150, 160	eleq12d 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
162	161	3adant2l 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
163	139, 162	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
164	163	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
165	164	3expib 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
166	165	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 ∈ 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
167	109	3adant1 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
168		ssun2 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
170		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
171	170	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
172	171	biimpar 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
173	58	snid 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ dom 𝑥 ∈ {dom 𝑥}
174	173, 102	eleqtrri 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
175	172, 174	eqeltrrdi 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
176	68, 175	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
177	176	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
178		funssfv 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
179	167, 169, 177, 178	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
180	172	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
181		fveq2 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
182	58, 59	fvsn 7180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
183	181, 182	eqtr3di 2785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
184	180, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
185	68, 184	syl3an3 1163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
186	179, 185	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
187	186	3expa 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
188	187	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
189	158	3adant1l 1174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
190		fveq2 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑘 = 𝑚 → (𝑥‘𝑘) = (𝑥‘𝑚))
191	190	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (𝑥‘𝑘) = (𝑥‘𝑚))
192	191	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘𝑘) = (𝑥‘𝑚))
193	189, 192	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑚))
194	193	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑚)))
195	188, 194	eleq12d 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
196	195	3adant2l 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
197	196	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
198	197	3expib 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
199	198	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
200	166, 199	jaoi 853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
201	135, 200	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
202	201	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
203	134, 202	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
204	203	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205	204	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ suc 𝑚 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
206	205	3impd 1346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ suc 𝑚 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207	206	impd 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ suc 𝑚 → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
208	207	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
209	208	3adant3 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
210	133, 209	ralrimi 3252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
211		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
212	211	feq2d 6702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
213		raleq 3320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → (∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
214	212, 213	3anbi13d 1436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
215	214	rspcev 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
216	56, 97, 126, 210, 215	syl13anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217		snex 5430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} ∈ V
218	32, 217	unex 7735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
219	22, 23, 218	axdc3lem3 10449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220	216, 219	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
221	220	3coml 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
222	221	3exp 1117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
223	222	expd 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → (𝑧 ∈ 𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
224	53, 223	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
225	224	3impd 1346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
226	225	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚⟶𝐴 → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
227	226	com23 86	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥:suc 𝑚⟶𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
228	49, 227	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229	228	imp 405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
230		resundir 5995	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
231		frel 6721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥:suc 𝑚⟶𝐴 → Rel 𝑥)
232		resdm 6025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
233	231, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
234	233	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
235	68, 72	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → dom 𝑥 ∈ ω)
236	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
237		incom 4200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
238	237	eqeq1i 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
239	58, 59	fnsn 6605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
240		fnresdisj 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
241	239, 240	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
242	238, 241, 104	3bitr3ri 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
243	236, 242	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
244	235, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245	234, 244	uneq12d 4163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
246		un0 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∪ ∅) = 𝑥
247	245, 246	eqtrdi 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
248	230, 247	eqtrid 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
249	248	ancoms 457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
250	249	3adant1 1128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
251	250	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252	251	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253	102	uneq2i 4159	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
254		dmun 5909	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
255		df-suc 6369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
256	253, 254, 255	3eqtr4i 2768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
257	252, 256	jctil 518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
258		dmeq 5902	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
259	258	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
260		reseq1 5974	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
261	260	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
262	259, 261	anbi12d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
263	262	rspcev 3611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
264	229, 257, 263	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
265	264	3exp2 1352	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
266	265	exlimdv 1934	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
267	266	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
268	48, 267	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
269	268	com3r 87	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
270	34, 269	mpan2d 690	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
271	270	com3r 87	. . . . . . . . . . . . . 14 ⊢ ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
272	271	3expd 1351	. . . . . . . . . . . . 13 ⊢ ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
273	272	com3r 87	. . . . . . . . . . . 12 ⊢ (𝑥:suc 𝑚⟶𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
274	273	3imp 1109	. . . . . . . . . . 11 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275	274	com12 32	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
276	275	rexlimiv 3146	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
277	33, 276	sylbi 216	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
278	277	impcom 406	. . . . . . 7 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
279		rabn0 4384	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
280	278, 279	sylibr 233	. . . . . 6 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
281	28	rabex 5331	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
282	281	elsn 4642	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
283	282	necon3bbii 2986	. . . . . 6 ⊢ (¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284	280, 283	sylibr 233	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
285	31, 284	eldifd 3958	. . . 4 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
286		axdc3lem4.3	. . . 4 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
287	285, 286	fmptd 7114	. . 3 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
288	28	axdc2 10446	. . 3 ⊢ ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
289	27, 287, 288	syl2an 594	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
290	22, 23, 286	axdc3lem2 10448	. 2 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
291	289, 290	syl 17	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539  ∃wex 1779   ∈ wcel 2104  {cab 2707   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  {crab 3430  Vcvv 3472   ∖ cdif 3944   ∪ cun 3945   ∩ cin 3946   ⊆ wss 3947  ∅c0 4321  𝒫 cpw 4601  {csn 4627  ⟨cop 4633   ↦ cmpt 5230  dom cdm 5675   ↾ cres 5677  Rel wrel 5680  Ord word 6362  suc csuc 6365  Fun wfun 6536   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  ωcom 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-dc 10443

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-om 7858  df-1o 8468

This theorem is referenced by:  axdc3  10451