Theorem axdc3lem4 10425

Description: Lemma for axdc3 10426. 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 10418 (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 10418 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 10421. See axdc3lem2 10423 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 7873	. . . . . 6 ⊢ ∅ ∈ ω
2		eqid 2765	. . . . . . . . . 10 ⊢ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3		fsng 7123	. . . . . . . . . . 11 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
4	1, 3	mpan 702	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
5	2, 4	mpbiri 261	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6		snssi 4747	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴)
7	5, 6	fssd 6713	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8		suc0 6427	. . . . . . . . 9 ⊢ suc ∅ = {∅}
9	8	feq2i 6687	. . . . . . . 8 ⊢ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
10	7, 9	sylibr 237	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11		fvsng 7168	. . . . . . . 8 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
12	1, 11	mpan 702	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13		ral0 4455	. . . . . . . 8 ⊢ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
14	13	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
15	10, 12, 14	3jca 1144	. . . . . 6 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16		suceq 6418	. . . . . . . . 9 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
17	16	feq2d 6679	. . . . . . . 8 ⊢ (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18		raleq 3320	. . . . . . . 8 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
19	17, 18	3anbi13d 1462	. . . . . . 7 ⊢ (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
20	19	rspcev 3584	. . . . . 6 ⊢ ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
21	1, 15, 20	sylancr 598	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22		axdc3lem4.1	. . . . . 6 ⊢ 𝐴 ∈ V
23		axdc3lem4.2	. . . . . 6 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
24		snex 5401	. . . . . 6 ⊢ {⟨∅, 𝐶⟩} ∈ V
25	22, 23, 24	axdc3lem3 10424	. . . . 5 ⊢ ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
26	21, 25	sylibr 237	. . . 4 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
27	26	ne0d 4297	. . 3 ⊢ (𝐶 ∈ 𝐴 → 𝑆 ≠ ∅)
28	22, 23	axdc3lem 10422	. . . . . . 7 ⊢ 𝑆 ∈ V
29		ssrab2 4036	. . . . . . 7 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
30	28, 29	elpwi2 5296	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
31	30	a1i 11	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
32		vex 3461	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
33	22, 23, 32	axdc3lem3 10424	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
34		simp2 1153	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → 𝑥:suc 𝑚⟶𝐴)
35		vex 3461	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑚 ∈ V
36	35	sucid 6434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑚 ∈ suc 𝑚
37		ffvelcdm 7066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑥‘𝑚) ∈ 𝐴)
38	36, 37	mpan2 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥‘𝑚) ∈ 𝐴)
39		ffvelcdm 7066	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥‘𝑚) ∈ 𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
40	38, 39	sylan2 604	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
41		eldifn 4088	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅})
42		fvex 6884	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘(𝑥‘𝑚)) ∈ V
43	42	elsn 4600	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) = ∅)
44	43	necon3bbii 3007	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) ≠ ∅)
45		n0 4308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑥‘𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
46	44, 45	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
47	41, 46	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
48	40, 47	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
49		simp32 1227	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → 𝑥:suc 𝑚⟶𝐴)
50		eldifi 4087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴)
51		elelpwi 4568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) → 𝑧 ∈ 𝐴)
52	51	expcom 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
53	40, 50, 52	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
54		peano2 7874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ ω → suc 𝑚 ∈ ω)
55	54	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → suc 𝑚 ∈ ω)
56	55	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
57		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥:suc 𝑚⟶𝐴)
58	32	dmex 7894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ dom 𝑥 ∈ V
59		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ 𝑧 ∈ V
60		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
61		fsng 7123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
62	60, 61	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
63	58, 59, 62	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
64		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
65	64	snssd 4748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {𝑧} ⊆ 𝐴)
66		fss 6712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
67	63, 65, 66	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
68		fdm 6705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → dom 𝑥 = suc 𝑚)
69	54	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
70		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
71	70	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
72	69, 71	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
73		nnord 7858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 ∈ ω → Ord dom 𝑥)
74		ordirr 6368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
75	72, 73, 74	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
76		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
77	76	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
78	75, 77	mtbid 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
79		disjsn 4673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
80	78, 79	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
81	68, 80	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
82	81	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
83	57, 67, 82	fun2d 6732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
84		sneq 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
85	84	uneq2d 4124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
86		df-suc 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
87	85, 86	eqtr4di 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
88	68, 87	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
89	88	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
90	89	feq2d 6679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
91	83, 90	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
92	91	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ 𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
93	92	adantrd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
94	93	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
95	94	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
96	95	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
97	96	3imp 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
98		ffun 6698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → Fun 𝑥)
99	98	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun 𝑥)
100	58, 59	funsn 6578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ Fun {⟨dom 𝑥, 𝑧⟩}
101	99, 100	jctir 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
102	59	dmsnop 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
103	102	ineq2i 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
104		disjsn 4673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
105	75, 104	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
106	103, 105	eqtrid 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
107	68, 106	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
108		funun 6571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
109	101, 107, 108	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
110		ssun1 4133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
111	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112		nnord 7858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑚 ∈ ω → Ord 𝑚)
113		0elsuc 7819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (Ord 𝑚 → ∅ ∈ suc 𝑚)
114	112, 113	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
115	114	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ suc 𝑚)
116	68	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
117	116	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
118	115, 117	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ dom 𝑥)
119		funssfv 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
120	109, 111, 118, 119	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
121	120	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
122	121	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
123	122	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
124	123	biimpar 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
125	124	adantrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
126	125	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
127		nfra1 3289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))
128		nfv 1937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑥:suc 𝑚⟶𝐴
129		nfv 1937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑚 ∈ ω
130	127, 128, 129	nf3an 1924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)
131		nfv 1937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐹‘(𝑥‘𝑚))
132		nfv 1937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)
133	130, 131, 132	nf3an 1924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶))
134		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ suc 𝑚)
135		elsuci 6419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ suc 𝑚 → (𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚))
136		rsp 3253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑘 ∈ 𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
137	136	impcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑘 ∈ 𝑚 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
138	137	ad2ant2lr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
139	138	3adant3 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
140	109	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
141	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
142		ordsucelsuc 7806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (Ord 𝑚 → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
143	112, 142	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑚 ∈ ω → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
144	143	biimpa 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → suc 𝑘 ∈ suc 𝑚)
145		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
146	145	biimparc 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
147	144, 68, 146	syl2an 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom 𝑥)
148		funssfv 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
149	140, 141, 147, 148	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
150	149	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
151	109	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
152	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
153		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚))
154	153	biimparc 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
155	68, 154	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
156	155	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
157		funssfv 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
158	151, 152, 156, 157	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
159	158	3adant1r 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
160	159	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑘)))
161	150, 160	eleq12d 2859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
162	161	3adant2l 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
163	139, 162	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
164	163	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
165	164	3expib 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
166	165	expcom 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 ∈ 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
167	109	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
168		ssun2 4134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
170		suceq 6418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
171	170	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
172	171	biimpar 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
173	58	snid 4624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ dom 𝑥 ∈ {dom 𝑥}
174	173, 102	eleqtrri 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
175	172, 174	eqeltrrdi 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
176	68, 175	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
177	176	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
178		funssfv 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
179	167, 169, 177, 178	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
180	172	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
181		fveq2 6871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
182	58, 59	fvsn 7169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
183	181, 182	eqtr3di 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
184	180, 183	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
185	68, 184	syl3an3 1181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
186	179, 185	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
187	186	3expa 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
188	187	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
189	158	3adant1l 1193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
190		fveq2 6871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑘 = 𝑚 → (𝑥‘𝑘) = (𝑥‘𝑚))
191	190	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (𝑥‘𝑘) = (𝑥‘𝑚))
192	191	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘𝑘) = (𝑥‘𝑚))
193	189, 192	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑚))
194	193	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑚)))
195	188, 194	eleq12d 2859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
196	195	3adant2l 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
197	196	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
198	197	3expib 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
199	198	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
200	166, 199	jaoi 870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
201	135, 200	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
202	201	com3r 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
203	134, 202	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
204	203	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205	204	expcom 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ suc 𝑚 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
206	205	3impd 1365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ suc 𝑚 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207	206	impd 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ suc 𝑚 → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
208	207	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
209	208	3adant3 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
210	133, 209	ralrimi 3263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
211		suceq 6418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
212	211	feq2d 6679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
213		raleq 3320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → (∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
214	212, 213	3anbi13d 1462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
215	214	rspcev 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
216	56, 97, 126, 210, 215	syl13anc 1395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217		snex 5401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} ∈ V
218	32, 217	unex 7731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
219	22, 23, 218	axdc3lem3 10424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220	216, 219	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
221	220	3coml 1143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
222	221	3exp 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
223	222	expd 420	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → (𝑧 ∈ 𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
224	53, 223	sylcom 31	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
225	224	3impd 1365	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
226	225	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚⟶𝐴 → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
227	226	com23 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥:suc 𝑚⟶𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
228	49, 227	mpdi 46	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229	228	imp 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
230		resundir 5984	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
231		frel 6701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥:suc 𝑚⟶𝐴 → Rel 𝑥)
232		resdm 6016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
233	231, 232	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
234	233	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
235	68, 72	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → dom 𝑥 ∈ ω)
236	73, 74	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
237		incom 4164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
238	237	eqeq1i 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
239	58, 59	fnsn 6583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
240		fnresdisj 6645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
241	239, 240	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
242	238, 241, 104	3bitr3ri 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
243	236, 242	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
244	235, 243	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245	234, 244	uneq12d 4125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
246		un0 4351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∪ ∅) = 𝑥
247	245, 246	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
248	230, 247	eqtrid 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
249	248	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
250	249	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
251	250	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252	251	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253	102	uneq2i 4121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
254		dmun 5891	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
255		df-suc 6356	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
256	253, 254, 255	3eqtr4i 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
257	252, 256	jctil 528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
258		dmeq 5884	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
259	258	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
260		reseq1 5963	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
261	260	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
262	259, 261	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
263	262	rspcev 3584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
264	229, 257, 263	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
265	264	3exp2 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
266	265	exlimdv 1956	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
267	266	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
268	48, 267	mpd 16	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
269	268	com3r 88	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
270	34, 269	mpan2d 706	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
271	270	com3r 88	. . . . . . . . . . . . . 14 ⊢ ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
272	271	3expd 1370	. . . . . . . . . . . . 13 ⊢ ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
273	272	com3r 88	. . . . . . . . . . . 12 ⊢ (𝑥:suc 𝑚⟶𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
274	273	3imp 1126	. . . . . . . . . . 11 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275	274	com12 33	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
276	275	rexlimiv 3159	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
277	33, 276	sylbi 220	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
278	277	impcom 412	. . . . . . 7 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
279		rabn0 4346	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
280	278, 279	sylibr 237	. . . . . 6 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
281	28	rabex 5300	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
282	281	elsn 4600	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
283	282	necon3bbii 3007	. . . . . 6 ⊢ (¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284	280, 283	sylibr 237	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
285	31, 284	eldifd 3918	. . . 4 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
286		axdc3lem4.3	. . . 4 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
287	285, 286	fmptd 7099	. . 3 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
288	28	axdc2 10421	. . 3 ⊢ ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
289	27, 287, 288	syl2an 607	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
290	22, 23, 286	axdc3lem2 10423	. 2 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
291	289, 290	syl 18	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145  {cab 2743   ≠ wne 2960  ∀wral 3079  ∃wrex 3089  {crab 3417  Vcvv 3457   ∖ cdif 3904   ∪ cun 3905   ∩ cin 3906   ⊆ wss 3907  ∅c0 4288  𝒫 cpw 4558  {csn 4585  ⟨cop 4591   ↦ cmpt 5186  dom cdm 5652   ↾ cres 5654  Rel wrel 5657  Ord word 6349  suc csuc 6352  Fun wfun 6519   Fn wfn 6520  ⟶wf 6521  ‘cfv 6525  ωcom 7850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-dc 10418

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-om 7851  df-1o 8441

This theorem is referenced by:  axdc3  10426