Theorem axdc3lem4 9874

Description: Lemma for axdc3 9875. 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 9867 (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 9867 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 9870. See axdc3lem2 9872 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 7600	. . . . . 6 ⊢ ∅ ∈ ω
2		eqid 2821	. . . . . . . . . 10 ⊢ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}
3		fsng 6898	. . . . . . . . . . 11 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
4	1, 3	mpan 688	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:{∅}⟶{𝐶} ↔ {⟨∅, 𝐶⟩} = {⟨∅, 𝐶⟩}))
5	2, 4	mpbiri 260	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶{𝐶})
6		snssi 4740	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴)
7	5, 6	fssd 6527	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
8		suc0 6264	. . . . . . . . 9 ⊢ suc ∅ = {∅}
9	8	feq2i 6505	. . . . . . . 8 ⊢ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ↔ {⟨∅, 𝐶⟩}:{∅}⟶𝐴)
10	7, 9	sylibr 236	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩}:suc ∅⟶𝐴)
11		fvsng 6941	. . . . . . . 8 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
12	1, 11	mpan 688	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}‘∅) = 𝐶)
13		ral0 4455	. . . . . . . 8 ⊢ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))
14	13	a1i 11	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))
15	10, 12, 14	3jca 1124	. . . . . 6 ⊢ (𝐶 ∈ 𝐴 → ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
16		suceq 6255	. . . . . . . . 9 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
17	16	feq2d 6499	. . . . . . . 8 ⊢ (𝑚 = ∅ → ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ↔ {⟨∅, 𝐶⟩}:suc ∅⟶𝐴))
18		raleq 3405	. . . . . . . 8 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)) ↔ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
19	17, 18	3anbi13d 1434	. . . . . . 7 ⊢ (𝑚 = ∅ → (({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))) ↔ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))))
20	19	rspcev 3622	. . . . . 6 ⊢ ((∅ ∈ ω ∧ ({⟨∅, 𝐶⟩}:suc ∅⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ ∅ ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘)))) → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
21	1, 15, 20	sylancr 589	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
22		axdc3lem4.1	. . . . . 6 ⊢ 𝐴 ∈ V
23		axdc3lem4.2	. . . . . 6 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
24		snex 5331	. . . . . 6 ⊢ {⟨∅, 𝐶⟩} ∈ V
25	22, 23, 24	axdc3lem3 9873	. . . . 5 ⊢ ({⟨∅, 𝐶⟩} ∈ 𝑆 ↔ ∃𝑚 ∈ ω ({⟨∅, 𝐶⟩}:suc 𝑚⟶𝐴 ∧ ({⟨∅, 𝐶⟩}‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 ({⟨∅, 𝐶⟩}‘suc 𝑘) ∈ (𝐹‘({⟨∅, 𝐶⟩}‘𝑘))))
26	21, 25	sylibr 236	. . . 4 ⊢ (𝐶 ∈ 𝐴 → {⟨∅, 𝐶⟩} ∈ 𝑆)
27	26	ne0d 4300	. . 3 ⊢ (𝐶 ∈ 𝐴 → 𝑆 ≠ ∅)
28	22, 23	axdc3lem 9871	. . . . . . 7 ⊢ 𝑆 ∈ V
29		ssrab2 4055	. . . . . . 7 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ⊆ 𝑆
30	28, 29	elpwi2 5248	. . . . . 6 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆
31	30	a1i 11	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ 𝒫 𝑆)
32		vex 3497	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
33	22, 23, 32	axdc3lem3 9873	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ ∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
34		simp2 1133	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → 𝑥:suc 𝑚⟶𝐴)
35		vex 3497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑚 ∈ V
36	35	sucid 6269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑚 ∈ suc 𝑚
37		ffvelrn 6848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑥‘𝑚) ∈ 𝐴)
38	36, 37	mpan2 689	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥‘𝑚) ∈ 𝐴)
39		ffvelrn 6848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑥‘𝑚) ∈ 𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
40	38, 39	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}))
41		eldifn 4103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅})
42		fvex 6682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹‘(𝑥‘𝑚)) ∈ V
43	42	elsn 4581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) = ∅)
44	43	necon3bbii 3063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ (𝐹‘(𝑥‘𝑚)) ≠ ∅)
45		n0 4309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘(𝑥‘𝑚)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
46	44, 45	bitri 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐹‘(𝑥‘𝑚)) ∈ {∅} ↔ ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
47	41, 46	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
48	40, 47	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)))
49		simp32 1206	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → 𝑥:suc 𝑚⟶𝐴)
50		eldifi 4102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴)
51		elelpwi 4550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴) → 𝑧 ∈ 𝐴)
52	51	expcom 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘(𝑥‘𝑚)) ∈ 𝒫 𝐴 → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
53	40, 50, 52	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → 𝑧 ∈ 𝐴))
54		peano2 7601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ ω → suc 𝑚 ∈ ω)
55	54	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → suc 𝑚 ∈ ω)
56	55	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → suc 𝑚 ∈ ω)
57		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥:suc 𝑚⟶𝐴)
58	32	dmex 7615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ dom 𝑥 ∈ V
59		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ 𝑧 ∈ V
60		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}
61		fsng 6898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → ({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ↔ {⟨dom 𝑥, 𝑧⟩} = {⟨dom 𝑥, 𝑧⟩}))
62	60, 61	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((dom 𝑥 ∈ V ∧ 𝑧 ∈ V) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧})
63	58, 59, 62	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧}
64		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
65	64	snssd 4741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {𝑧} ⊆ 𝐴)
66		fss 6526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (({⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶{𝑧} ∧ {𝑧} ⊆ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
67	63, 65, 66	sylancr 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → {⟨dom 𝑥, 𝑧⟩}:{dom 𝑥}⟶𝐴)
68		fdm 6521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → dom 𝑥 = suc 𝑚)
69	54	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → suc 𝑚 ∈ ω)
70		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
71	70	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ ω ↔ suc 𝑚 ∈ ω))
72	69, 71	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 ∈ ω)
73		nnord 7587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 ∈ ω → Ord dom 𝑥)
74		ordirr 6208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (Ord dom 𝑥 → ¬ dom 𝑥 ∈ dom 𝑥)
75	72, 73, 74	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ dom 𝑥)
76		eleq2 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (dom 𝑥 = suc 𝑚 → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
77	76	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∈ dom 𝑥 ↔ dom 𝑥 ∈ suc 𝑚))
78	75, 77	mtbid 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ¬ dom 𝑥 ∈ suc 𝑚)
79		disjsn 4646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((suc 𝑚 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ suc 𝑚)
80	78, 79	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
81	68, 80	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
82	81	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∩ {dom 𝑥}) = ∅)
83	57, 67, 82	fun2d 6541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴)
84		sneq 4576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (dom 𝑥 = suc 𝑚 → {dom 𝑥} = {suc 𝑚})
85	84	uneq2d 4138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = (suc 𝑚 ∪ {suc 𝑚}))
86		df-suc 6196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ suc suc 𝑚 = (suc 𝑚 ∪ {suc 𝑚})
87	85, 86	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
88	68, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
89	88	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (suc 𝑚 ∪ {dom 𝑥}) = suc suc 𝑚)
90	89	feq2d 6499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):(suc 𝑚 ∪ {dom 𝑥})⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
91	83, 90	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
92	91	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ 𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
93	92	adantrd 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
94	93	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
95	94	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
96	95	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)))
97	96	3imp 1107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴)
98		ffun 6516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥:suc 𝑚⟶𝐴 → Fun 𝑥)
99	98	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun 𝑥)
100	58, 59	funsn 6406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ Fun {⟨dom 𝑥, 𝑧⟩}
101	99, 100	jctir 523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}))
102	59	dmsnop 6072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ dom {⟨dom 𝑥, 𝑧⟩} = {dom 𝑥}
103	102	ineq2i 4185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∩ {dom 𝑥})
104		disjsn 4646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((dom 𝑥 ∩ {dom 𝑥}) = ∅ ↔ ¬ dom 𝑥 ∈ dom 𝑥)
105	75, 104	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ {dom 𝑥}) = ∅)
106	103, 105	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
107	68, 106	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅)
108		funun 6399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((Fun 𝑥 ∧ Fun {⟨dom 𝑥, 𝑧⟩}) ∧ (dom 𝑥 ∩ dom {⟨dom 𝑥, 𝑧⟩}) = ∅) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
109	101, 107, 108	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
110		ssun1 4147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
111	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
112		nnord 7587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑚 ∈ ω → Ord 𝑚)
113		0elsuc 7549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (Ord 𝑚 → ∅ ∈ suc 𝑚)
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ ω → ∅ ∈ suc 𝑚)
115	114	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ suc 𝑚)
116	68	eleq2d 2898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥:suc 𝑚⟶𝐴 → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
117	116	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (∅ ∈ dom 𝑥 ↔ ∅ ∈ suc 𝑚))
118	115, 117	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ∅ ∈ dom 𝑥)
119		funssfv 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ ∅ ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
120	109, 111, 118, 119	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = (𝑥‘∅))
121	120	eqeq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
122	121	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
123	122	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ↔ (𝑥‘∅) = 𝐶))
124	123	biimpar 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑥‘∅) = 𝐶) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
125	124	adantrl 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
126	125	3adant2 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶)
127		nfra1 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))
128		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑥:suc 𝑚⟶𝐴
129		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ Ⅎ𝑘 𝑚 ∈ ω
130	127, 128, 129	nf3an 1898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)
131		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐹‘(𝑥‘𝑚))
132		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑘(𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)
133	130, 131, 132	nf3an 1898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶))
134		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ suc 𝑚)
135		elsuci 6256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ suc 𝑚 → (𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚))
136		rsp 3205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑘 ∈ 𝑚 → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
137	136	impcom 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑘 ∈ 𝑚 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
138	137	ad2ant2lr 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚)) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
139	138	3adant3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)))
140	109	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
141	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
142		ordsucelsuc 7536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (Ord 𝑚 → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
143	112, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (𝑚 ∈ ω → (𝑘 ∈ 𝑚 ↔ suc 𝑘 ∈ suc 𝑚))
144	143	biimpa 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → suc 𝑘 ∈ suc 𝑚)
145		eleq2 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑚 → (suc 𝑘 ∈ dom 𝑥 ↔ suc 𝑘 ∈ suc 𝑚))
146	145	biimparc 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((suc 𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom 𝑥)
147	144, 68, 146	syl2an 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom 𝑥)
148		funssfv 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
149	140, 141, 147, 148	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
150	149	3adant2 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = (𝑥‘suc 𝑘))
151	109	3adant2 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
152	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
153		eleq2 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ (dom 𝑥 = suc 𝑚 → (𝑘 ∈ dom 𝑥 ↔ 𝑘 ∈ suc 𝑚))
154	153	biimparc 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 ∈ suc 𝑚 ∧ dom 𝑥 = suc 𝑚) → 𝑘 ∈ dom 𝑥)
155	68, 154	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
156	155	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → 𝑘 ∈ dom 𝑥)
157		funssfv 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑥 ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ 𝑘 ∈ dom 𝑥) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
158	151, 152, 156, 157	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
159	158	3adant1r 1173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
160	159	fveq2d 6673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑘)))
161	150, 160	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
162	161	3adant2l 1174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))))
163	139, 162	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
164	163	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
165	164	3expib 1118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ ω ∧ 𝑘 ∈ 𝑚) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
166	165	expcom 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 ∈ 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
167	109	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
168		ssun2 4148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
170		suceq 6255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ (𝑘 = 𝑚 → suc 𝑘 = suc 𝑚)
171	170	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑘 = 𝑚 → (dom 𝑥 = suc 𝑘 ↔ dom 𝑥 = suc 𝑚))
172	171	biimpar 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
173	58	snid 4600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ dom 𝑥 ∈ {dom 𝑥}
174	173, 102	eleqtrri 2912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ dom 𝑥 ∈ dom {⟨dom 𝑥, 𝑧⟩}
175	172, 174	eqeltrrdi 2922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑘 = 𝑚 ∧ dom 𝑥 = suc 𝑚) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
176	68, 175	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
177	176	3adant2 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩})
178		funssfv 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((Fun (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ {⟨dom 𝑥, 𝑧⟩} ⊆ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∧ suc 𝑘 ∈ dom {⟨dom 𝑥, 𝑧⟩}) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
179	167, 169, 177, 178	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
180	172	3adant2 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → dom 𝑥 = suc 𝑘)
181	58, 59	fvsn 6942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = 𝑧
182		fveq2 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘dom 𝑥) = ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘))
183	181, 182	syl5reqr 2871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (dom 𝑥 = suc 𝑘 → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
184	180, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ dom 𝑥 = suc 𝑚) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
185	68, 184	syl3an3 1161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩}‘suc 𝑘) = 𝑧)
186	179, 185	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
187	186	3expa 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
188	187	3adant2 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) = 𝑧)
189	158	3adant1l 1172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑘))
190		fveq2 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (𝑘 = 𝑚 → (𝑥‘𝑘) = (𝑥‘𝑚))
191	190	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (𝑥‘𝑘) = (𝑥‘𝑚))
192	191	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥‘𝑘) = (𝑥‘𝑚))
193	189, 192	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘) = (𝑥‘𝑚))
194	193	fveq2d 6673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) = (𝐹‘(𝑥‘𝑚)))
195	188, 194	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ 𝑘 ∈ suc 𝑚 ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
196	195	3adant2l 1174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))))
197	196	biimprd 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
198	197	3expib 1118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑘 = 𝑚 ∧ 𝑚 ∈ ω) → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
199	198	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
200	166, 199	jaoi 853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑘 ∈ 𝑚 ∨ 𝑘 = 𝑚) → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
201	135, 200	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
202	201	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑘 ∈ suc 𝑚 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
203	134, 202	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
204	203	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑘 ∈ suc 𝑚) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))))
205	204	expcom 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ suc 𝑚 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))))
206	205	3impd 1344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ suc 𝑚 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
207	206	impd 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ suc 𝑚 → (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
208	207	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚))) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
209	208	3adant3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑘 ∈ suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
210	133, 209	ralrimi 3216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))
211		suceq 6255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑝 = suc 𝑚 → suc 𝑝 = suc suc 𝑚)
212	211	feq2d 6499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ↔ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴))
213		raleq 3405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑝 = suc 𝑚 → (∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)) ↔ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
214	212, 213	3anbi13d 1434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑝 = suc 𝑚 → (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))) ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))))
215	214	rspcev 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((suc 𝑚 ∈ ω ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc suc 𝑚⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ suc 𝑚((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘)))) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
216	56, 97, 126, 210, 215	syl13anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
217		snex 5331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} ∈ V
218	32, 217	unex 7468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ V
219	22, 23, 218	axdc3lem3 9873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ↔ ∃𝑝 ∈ ω ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}):suc 𝑝⟶𝐴 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑝 ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘suc 𝑘) ∈ (𝐹‘((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩})‘𝑘))))
220	216, 219	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) ∧ 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
221	220	3coml 1123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
222	221	3exp 1115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑧 ∈ 𝐴 ∧ (𝑥‘∅) = 𝐶) → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
223	222	expd 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → (𝑧 ∈ 𝐴 → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
224	53, 223	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))))
225	224	3impd 1344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
226	225	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑥:suc 𝑚⟶𝐴 → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
227	226	com23 86	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥:suc 𝑚⟶𝐴 → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)))
228	49, 227	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆))
229	228	imp 409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆)
230		resundir 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥))
231		frel 6518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥:suc 𝑚⟶𝐴 → Rel 𝑥)
232		resdm 5896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Rel 𝑥 → (𝑥 ↾ dom 𝑥) = 𝑥)
233	231, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥:suc 𝑚⟶𝐴 → (𝑥 ↾ dom 𝑥) = 𝑥)
234	233	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → (𝑥 ↾ dom 𝑥) = 𝑥)
235	68, 72	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → dom 𝑥 ∈ ω)
236	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑥 ∈ ω → ¬ dom 𝑥 ∈ dom 𝑥)
237		incom 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({dom 𝑥} ∩ dom 𝑥) = (dom 𝑥 ∩ {dom 𝑥})
238	237	eqeq1i 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ (dom 𝑥 ∩ {dom 𝑥}) = ∅)
239	58, 59	fnsn 6411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥}
240		fnresdisj 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({⟨dom 𝑥, 𝑧⟩} Fn {dom 𝑥} → (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅))
241	239, 240	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (({dom 𝑥} ∩ dom 𝑥) = ∅ ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
242	238, 241, 104	3bitr3ri 304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (¬ dom 𝑥 ∈ dom 𝑥 ↔ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
243	236, 242	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑥 ∈ ω → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
244	235, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥) = ∅)
245	234, 244	uneq12d 4139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = (𝑥 ∪ ∅))
246		un0 4343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∪ ∅) = 𝑥
247	245, 246	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ↾ dom 𝑥) ∪ ({⟨dom 𝑥, 𝑧⟩} ↾ dom 𝑥)) = 𝑥)
248	230, 247	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ω ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
249	248	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
250	249	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
251	250	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω)) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
252	251	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)
253	102	uneq2i 4135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ {dom 𝑥})
254		dmun 5778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 𝑧⟩})
255		df-suc 6196	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
256	253, 254, 255	3eqtr4i 2854	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥
257	252, 256	jctil 522	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
258		dmeq 5771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → dom 𝑦 = dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}))
259	258	eqeq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (dom 𝑦 = suc dom 𝑥 ↔ dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥))
260		reseq1 5846	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → (𝑦 ↾ dom 𝑥) = ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥))
261	260	eqeq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥))
262	259, 261	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)))
263	262	rspcev 3622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ∈ 𝑆 ∧ (dom (𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) = suc dom 𝑥 ∧ ((𝑥 ∪ {⟨dom 𝑥, 𝑧⟩}) ↾ dom 𝑥) = 𝑥)) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
264	229, 257, 263	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) ∧ (𝑥‘∅) = 𝐶 ∧ (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω))) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
265	264	3exp2 1350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
266	265	exlimdv 1930	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
267	266	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → (∃𝑧 𝑧 ∈ (𝐹‘(𝑥‘𝑚)) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))))
268	48, 267	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
269	268	com3r 87	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥:suc 𝑚⟶𝐴) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
270	34, 269	mpan2d 692	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥‘∅) = 𝐶 → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
271	270	com3r 87	. . . . . . . . . . . . . 14 ⊢ ((𝑥‘∅) = 𝐶 → ((∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) ∧ 𝑥:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ ω) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
272	271	3expd 1349	. . . . . . . . . . . . 13 ⊢ ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑥:suc 𝑚⟶𝐴 → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
273	272	com3r 87	. . . . . . . . . . . 12 ⊢ (𝑥:suc 𝑚⟶𝐴 → ((𝑥‘∅) = 𝐶 → (∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘)) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))))
274	273	3imp 1107	. . . . . . . . . . 11 ⊢ ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝑚 ∈ ω → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
275	274	com12 32	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))))
276	275	rexlimiv 3280	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ω (𝑥:suc 𝑚⟶𝐴 ∧ (𝑥‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑚 (𝑥‘suc 𝑘) ∈ (𝐹‘(𝑥‘𝑘))) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
277	33, 276	sylbi 219	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑆 → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)))
278	277	impcom 410	. . . . . . 7 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
279		rabn0 4338	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑆 (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥))
280	278, 279	sylibr 236	. . . . . 6 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
281	28	rabex 5234	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ V
282	281	elsn 4581	. . . . . . 7 ⊢ ({𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = ∅)
283	282	necon3bbii 3063	. . . . . 6 ⊢ (¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅} ↔ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ≠ ∅)
284	280, 283	sylibr 236	. . . . 5 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → ¬ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ {∅})
285	31, 284	eldifd 3946	. . . 4 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝑆) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} ∈ (𝒫 𝑆 ∖ {∅}))
286		axdc3lem4.3	. . . 4 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
287	285, 286	fmptd 6877	. . 3 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅}))
288	28	axdc2 9870	. . 3 ⊢ ((𝑆 ≠ ∅ ∧ 𝐺:𝑆⟶(𝒫 𝑆 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
289	27, 287, 288	syl2an 597	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
290	22, 23, 286	axdc3lem2 9872	. 2 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
291	289, 290	syl 17	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1533  ∃wex 1776   ∈ wcel 2110  {cab 2799   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3494   ∖ cdif 3932   ∪ cun 3933   ∩ cin 3934   ⊆ wss 3935  ∅c0 4290  𝒫 cpw 4538  {csn 4566  ⟨cop 4572   ↦ cmpt 5145  dom cdm 5554   ↾ cres 5556  Rel wrel 5559  Ord word 6189  suc csuc 6192  Fun wfun 6348   Fn wfn 6349  ⟶wf 6350  ‘cfv 6354  ωcom 7579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-dc 9867

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-om 7580  df-1o 8101

This theorem is referenced by:  axdc3  9875