Theorem axdc3lem4 10459

Description: Lemma for axdc3 10460. 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 10452 (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 10452 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 10455. See axdc3lem2 10457 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 7889	. . . . . 6 ⊢ ∅ ∈ ω
2		eqid 2762	. . . . . . . . . 10 ⊢ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3		fsng 7135	. . . . . . . . . . 11 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
4	1, 3	mpan 703	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
5	2, 4	mpbiri 261	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6		snssi 4749	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴)
7	5, 6	fssd 6724	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8		suc0 6439	. . . . . . . . 9 ⊢ suc ∅ = {∅}
9	8	feq2i 6698	. . . . . . . 8 ⊢ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
10	7, 9	sylibr 237	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11		fvsng 7182	. . . . . . . 8 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
12	1, 11	mpan 703	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13		ral0 4457	. . . . . . . 8 ⊢ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
14	13	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
15	10, 12, 14	3jca 1146	. . . . . 6 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16		suceq 6430	. . . . . . . . 9 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
17	16	feq2d 6690	. . . . . . . 8 ⊢ (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18		raleq 3318	. . . . . . . 8 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
19	17, 18	3anbi13d 1466	. . . . . . 7 ⊢ (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
20	19	rspcev 3579	. . . . . 6 ⊢ ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
21	1, 15, 20	sylancr 599	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22		axdc3lem4.1	. . . . . 6 ⊢ 𝐴 ∈ V
23		axdc3lem4.2	. . . . . 6 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
24		snex 5408	. . . . . 6 ⊢ {⟨∅, 𝐶⟩} ∈ V
25	22, 23, 24	axdc3lem3 10458	. . . . 5 ⊢ ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
26	21, 25	sylibr 237	. . . 4 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
27	26	ne0d 4291	. . 3 ⊢ (𝐶 ∈ 𝐴 → 𝑆 ≠ ∅)
28	22, 23	axdc3lem 10456	. . . . . . 7 ⊢ 𝑆 ∈ V
29		ssrab2 4031	. . . . . . 7 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
30	28, 29	elpwi2 5304	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
31	30	a1i 11	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
32		vex 3457	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
33	22, 23, 32	axdc3lem3 10458	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
34		simp2 1155	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → 𝑥:suc 𝑚⟶𝐴)
35		vex 3457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑚 ∈ V
36	35	sucid 6446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑚 ∈ suc 𝑚
37		ffvelcdm 7078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑥‘𝑚) ∈ 𝐴)
38	36, 37	mpan2 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥‘𝑚) ∈ 𝐴)
39		ffvelcdm 7078	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥‘𝑚) ∈ 𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
40	38, 39	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
41		eldifn 4082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅})
42		fvex 6895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘(𝑥‘𝑚)) ∈ V
43	42	elsn 4602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) = ∅)
44	43	necon3bbii 3004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) ≠ ∅)
45		n0 4303	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑥‘𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
46	44, 45	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
47	41, 46	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
48	40, 47	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
49		simp32 1229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → 𝑥:suc 𝑚⟶𝐴)
50		eldifi 4081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴)
51		elelpwi 4570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) → 𝑧 ∈ 𝐴)
52	51	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
53	40, 50, 52	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
54		peano2 7890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ ω → suc 𝑚 ∈ ω)
55	54	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → suc 𝑚 ∈ ω)
56	55	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
57		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥:suc 𝑚⟶𝐴)
58	32	dmex 7910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ dom 𝑥 ∈ V
59		vex 3457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ 𝑧 ∈ V
60		eqid 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
61		fsng 7135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
62	60, 61	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
63	58, 59, 62	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
64		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
65	64	snssd 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {𝑧} ⊆ 𝐴)
66		fss 6723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
67	63, 65, 66	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
68		fdm 6716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → dom 𝑥 = suc 𝑚)
69	54	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
70		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
71	70	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
72	69, 71	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
73		nnord 7874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 ∈ ω → Ord dom 𝑥)
74		ordirr 6379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
75	72, 73, 74	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
76		eleq2 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
77	76	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
78	75, 77	mtbid 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
79		disjsn 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
80	78, 79	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
81	68, 80	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
82	81	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
83	57, 67, 82	fun2d 6743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
84		sneq 4597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
85	84	uneq2d 4118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
86		df-suc 6367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
87	85, 86	eqtr4di 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
88	68, 87	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
89	88	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
90	89	feq2d 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
91	83, 90	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
92	91	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ 𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
93	92	adantrd 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
94	93	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
95	94	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
96	95	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
97	96	3imp 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
98		ffun 6709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → Fun 𝑥)
99	98	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun 𝑥)
100	58, 59	funsn 6590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ Fun {⟨dom 𝑥, 𝑧⟩}
101	99, 100	jctir 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
102	59	dmsnop 6216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
103	102	ineq2i 4166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
104		disjsn 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
105	75, 104	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
106	103, 105	eqtrid 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
107	68, 106	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
108		funun 6583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
109	101, 107, 108	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
110		ssun1 4127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
111	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112		nnord 7874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑚 ∈ ω → Ord 𝑚)
113		0elsuc 7835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (Ord 𝑚 → ∅ ∈ suc 𝑚)
114	112, 113	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
115	114	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ suc 𝑚)
116	68	eleq2d 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
117	116	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
118	115, 117	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ dom 𝑥)
119		funssfv 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
120	109, 111, 118, 119	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
121	120	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
122	121	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
123	122	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
124	123	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
125	124	adantrl 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
126	125	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
127		nfra1 3288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))
128		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑥:suc 𝑚⟶𝐴
129		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑚 ∈ ω
130	127, 128, 129	nf3an 1934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)
131		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐹‘(𝑥‘𝑚))
132		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)
133	130, 131, 132	nf3an 1934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶))
134		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ suc 𝑚)
135		elsuci 6431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ suc 𝑚 → (𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚))
136		rsp 3252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑘 ∈ 𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
137	136	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑘 ∈ 𝑚 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
138	137	ad2ant2lr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
139	138	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
140	109	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
141	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
142		ordsucelsuc 7822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (Ord 𝑚 → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
143	112, 142	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑚 ∈ ω → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
144	143	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → suc 𝑘 ∈ suc 𝑚)
145		eleq2 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
146	145	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
147	144, 68, 146	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom 𝑥)
148		funssfv 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
149	140, 141, 147, 148	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
150	149	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
151	109	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
152	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
153		eleq2 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚))
154	153	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
155	68, 154	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
156	155	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
157		funssfv 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
158	151, 152, 156, 157	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
159	158	3adant1r 1196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
160	159	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑘)))
161	150, 160	eleq12d 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
162	161	3adant2l 1197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
166	165	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 ∈ 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
167	109	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
168		ssun2 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
170		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
171	170	eqeq2d 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
172	171	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
173	58	snid 4626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ dom 𝑥 ∈ {dom 𝑥}
174	173, 102	eleqtrri 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
175	172, 174	eqeltrrdi 2871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
176	68, 175	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
177	176	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
178		funssfv 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
179	167, 169, 177, 178	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
180	172	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
181		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
182	58, 59	fvsn 7183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
183	181, 182	eqtr3di 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
184	180, 183	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
185	68, 184	syl3an3 1183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
186	179, 185	eqtrd 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
187	186	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
188	187	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
189	158	3adant1l 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
190		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑘 = 𝑚 → (𝑥‘𝑘) = (𝑥‘𝑚))
191	190	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (𝑥‘𝑘) = (𝑥‘𝑚))
192	191	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘𝑘) = (𝑥‘𝑚))
193	189, 192	eqtrd 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑚))
194	193	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑚)))
195	188, 194	eleq12d 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
196	195	3adant2l 1197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
197	196	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
198	197	3expib 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
199	198	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
200	166, 199	jaoi 871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205	204	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ suc 𝑚 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
206	205	3impd 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ suc 𝑚 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207	206	impd 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ suc 𝑚 → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
208	207	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
209	208	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
210	133, 209	ralrimi 3262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
211		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
212	211	feq2d 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
213		raleq 3318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → (∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
214	212, 213	3anbi13d 1466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
215	214	rspcev 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
216	56, 97, 126, 210, 215	syl13anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217		snex 5408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} ∈ V
218	32, 217	unex 7750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
219	22, 23, 218	axdc3lem3 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220	216, 219	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
221	220	3coml 1145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
222	221	3exp 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
223	222	expd 421	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → (𝑧 ∈ 𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
224	53, 223	sylcom 31	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
225	224	3impd 1367	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
226	225	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
230		resundir 5991	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
231		frel 6712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥:suc 𝑚⟶𝐴 → Rel 𝑥)
232		resdm 6023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
233	231, 232	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
234	233	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
235	68, 72	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → dom 𝑥 ∈ ω)
236	73, 74	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
237		incom 4158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
238	237	eqeq1i 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
239	58, 59	fnsn 6595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
240		fnresdisj 6656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
246		un0 4347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∪ ∅) = 𝑥
247	245, 246	eqtrdi 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
248	230, 247	eqtrid 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
249	248	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
250	249	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
251	250	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252	251	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253	102	uneq2i 4115	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
254		dmun 5898	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
255		df-suc 6367	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
256	253, 254, 255	3eqtr4i 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
257	252, 256	jctil 529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
258		dmeq 5891	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
259	258	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
260		reseq1 5970	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
261	260	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
262	259, 261	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
263	262	rspcev 3579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
264	229, 257, 263	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
265	264	3exp2 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
266	265	exlimdv 1966	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
267	266	adantr 486	. . . . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
271	270	com3r 88	. . . . . . . . . . . . . 14 ⊢ ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
272	271	3expd 1372	. . . . . . . . . . . . 13 ⊢ ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
273	272	com3r 88	. . . . . . . . . . . 12 ⊢ (𝑥:suc 𝑚⟶𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
274	273	3imp 1128	. . . . . . . . . . 11 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275	274	com12 33	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
276	275	rexlimiv 3158	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
277	33, 276	sylbi 220	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
278	277	impcom 413	. . . . . . 7 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
279		rabn0 4342	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
280	278, 279	sylibr 237	. . . . . 6 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
281	28	rabex 5307	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
282	281	elsn 4602	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
283	282	necon3bbii 3004	. . . . . 6 ⊢ (¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284	280, 283	sylibr 237	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
285	31, 284	eldifd 3913	. . . 4 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
286		axdc3lem4.3	. . . 4 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
287	285, 286	fmptd 7111	. . 3 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
288	28	axdc2 10455	. . 3 ⊢ ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
289	27, 287, 288	syl2an 608	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
290	22, 23, 286	axdc3lem2 10457	. 2 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
291	289, 290	syl 18	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2740   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  {crab 3414  Vcvv 3453   ∖ cdif 3899   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282  𝒫 cpw 4560  {csn 4587  ⟨cop 4593   ↦ cmpt 5190  dom cdm 5659   ↾ cres 5661  Rel wrel 5664  Ord word 6360  suc csuc 6363  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  ωcom 7866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-dc 10452

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-om 7867  df-1o 8459

This theorem is used by:  axdc3  10460