Theorem cfsmolem 10186

Description: Lemma for cfsmo 10187. (Contributed by Mario Carneiro, 28-Feb-2013.)

Hypotheses

Ref	Expression
cfsmolem.2	⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)))
cfsmolem.3	⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))

Assertion

Ref	Expression
cfsmolem	⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))

Distinct variable groups:   𝑓,𝑔,𝑡,𝑤,𝑧,𝐴   𝑓,𝐹,𝑡,𝑧   𝑓,𝐺,𝑤,𝑧

Allowed substitution hints:   𝐹(𝑤,𝑔)   𝐺(𝑡,𝑔)

Proof of Theorem cfsmolem

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cff1 10174	. 2 ⊢ (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)))
2		cfon 10171	. . . . . . . . . . . 12 ⊢ (cf‘𝐴) ∈ On
3	2	oneli 6433	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On)
4	3	3ad2ant3 1136	. . . . . . . . . 10 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
5		eleq1w 2820	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴)))
6	5	3anbi3d 1445	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴))))
7		fveq2 6835	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦))
8	7	eleq1d 2822	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝐺‘𝑥) ∈ 𝐴 ↔ (𝐺‘𝑦) ∈ 𝐴))
9	6, 8	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴)))
10		simpl1 1193	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑔:(cf‘𝐴)–1-1→𝐴)
11		simpl2 1194	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
12		ontr1 6365	. . . . . . . . . . . . . . . . . 18 ⊢ ((cf‘𝐴) ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)))
13	2, 12	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))
14	13	ancoms 458	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴))
15	14	3ad2antl3 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴))
16		pm2.27 42	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
17	10, 11, 15, 16	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
18	17	ralimdva 3150	. . . . . . . . . . . . 13 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴))
19		cfsmolem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))
20	19	fveq1i 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥)
21		fvres 6854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥))
22	20, 21	eqtrid 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥))
23		recsval 8337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥)))
24		recsfnon 8336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ recs(𝐹) Fn On
25		fnfun 6593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (recs(𝐹) Fn On → Fun recs(𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun recs(𝐹)
27		vex 3434	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑥 ∈ V
28		resfunexg 7164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V)
29	26, 27, 28	mp2an 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (recs(𝐹) ↾ 𝑥) ∈ V
30		dmeq 5853	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥))
31	30	fveq2d 6839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥)))
32		fveq1 6834	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡))
33		suceq 6386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
35	30, 34	iuneq12d 4964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡) = ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
36	31, 35	uneq12d 4110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
37		cfsmolem.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)))
38		fvex 6848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V
39	29	dmex 7854	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ dom (recs(𝐹) ↾ 𝑥) ∈ V
40		fvex 6848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
41	40	sucex 7754	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
42	39, 41	iunex 7915	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
43	38, 42	unex 7692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V
44	36, 37, 43	fvmpt 6942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((recs(𝐹) ↾ 𝑥) ∈ V → (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
45	29, 44	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
46	23, 45	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
47		onss 7733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
48		fnssres 6616	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((recs(𝐹) Fn On ∧ 𝑥 ⊆ On) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
49	24, 47, 48	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
50		fndm 6596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥)
51		fveq2 6835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔‘𝑥))
52		iuneq1 4951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
53		fvres 6854	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡))
54		suceq 6386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ 𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
56	55	iuneq2i 4956	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)
57		fveq2 6835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡))
58		suceq 6386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
60	59	cbviunv 4982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)
61	56, 60	eqtr4i 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)
62	52, 61	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
63	51, 62	uneq12d 4110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
64	49, 50, 63	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
65	46, 64	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
66	3, 65	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
67	22, 66	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
68	67	3ad2ant2 1135	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
69		eloni 6328	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ On → Ord 𝐴)
70	69	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Ord 𝐴)
71	70	3ad2ant1 1134	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → Ord 𝐴)
72		f1f 6731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:(cf‘𝐴)–1-1→𝐴 → 𝑔:(cf‘𝐴)⟶𝐴)
73	72	ffvelcdmda 7031	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴)
74	73	adantlr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴)
75	74	3adant3 1133	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝑔‘𝑥) ∈ 𝐴)
76	19	fveq1i 6836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺‘𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦)
77	13	fvresd 6855	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦))
78	76, 77	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
79	78	adantrl 717	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
80	79	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
81	80	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴))
82		ordsucss 7763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
83	69, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
84	83	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
85	81, 84	sylbid 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
86	85	ralimdva 3150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
87		iunss 4988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
88	86, 87	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
89	88	3impia 1118	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
90		onelon 6343	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On)
91	90	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
92	91	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
93	81, 92	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
94		onsuc 7758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On)
95	93, 94	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On))
96	95	ralimdva 3150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On))
97	96	3impia 1118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
98		iunon 8273	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
99	27, 97, 98	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
100		simp1 1137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → 𝐴 ∈ On)
101		onsseleq 6359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
102	99, 100, 101	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
103		idd 24	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
104		simpll 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴))
105		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝐴 ∈ On)
106	3	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ On)
107	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
108	107	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
109	78	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
110		fvres 6854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
111	110	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
112	109, 111	eqtr4d 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
113	112	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
114	113	ralbidva 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (cf‘𝐴) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 ↔ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
115	114	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
116		ffnfv 7066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
117	108, 115, 116	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴)
118		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ 𝐴))
119	118	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
120	119	adantrl 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
121	120	3adant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
122		onelon 6343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ On)
123	110	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
124		ffvelcdm 7028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
125	123, 124	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴)
126	125, 90	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
127	126	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
128		onsssuc 6410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
129	122, 127, 128	syl2an2r 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
130	129	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
131	130	rexbidva 3160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
132		eliun 4938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))
133	131, 132	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
134	133	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
135	134	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
136	121, 135	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
137	136	3expa 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
138	137	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
139	138	ralrimiva 3130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
140	139	expl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
141	117, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
142	141	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
143		feq1 6641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥⟶𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴))
144		fveq1 6834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
145	144	sseq2d 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓‘𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
146	145	rexbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
147	110	sseq2d 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ∈ 𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦)))
148	147	rexbiia 3083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
149	146, 148	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
150	149	ralbidv 3161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
151	143, 150	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))))
152	29, 151	spcev 3549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)))
153	117, 142, 152	syl2an2r 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)))
154		cfflb 10175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
155	154	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) → (cf‘𝐴) ⊆ 𝑥)
156	105, 106, 153, 155	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥)
157		ontri1 6352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((cf‘𝐴) ∈ On ∧ 𝑥 ∈ On) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
158	2, 3, 157	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
159	158	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
160	156, 159	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴))
161	104, 160	pm2.21dd 195	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
162	161	ex 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
163	162	expcomd 416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐴 ∈ On → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
164	163	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
165	164	3impib 1117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
166	103, 165	jaod 860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
167	102, 166	sylbid 240	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
168	89, 167	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
169	168	3adant1l 1178	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
170		ordunel 7772	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝐴 ∧ (𝑔‘𝑥) ∈ 𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
171	71, 75, 169, 170	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
172	68, 171	eqeltrd 2837	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐴)
173	172	3expia 1122	. . . . . . . . . . . . . 14 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴))
174	173	3impa 1110	. . . . . . . . . . . . 13 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴))
175	18, 174	syldc 48	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴))
176	175	a1i 11	. . . . . . . . . . 11 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)))
177	9, 176	tfis2 7802	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴))
178	4, 177	mpcom 38	. . . . . . . . 9 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)
179	178	3expia 1122	. . . . . . . 8 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) ∈ 𝐴))
180	179	ralrimiv 3129	. . . . . . 7 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)
181	2	onssi 7783	. . . . . . . . 9 ⊢ (cf‘𝐴) ⊆ On
182		fnssres 6616	. . . . . . . . . 10 ⊢ ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
183	19	fneq1i 6590	. . . . . . . . . 10 ⊢ (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
184	182, 183	sylibr 234	. . . . . . . . 9 ⊢ ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → 𝐺 Fn (cf‘𝐴))
185	24, 181, 184	mp2an 693	. . . . . . . 8 ⊢ 𝐺 Fn (cf‘𝐴)
186		ffnfv 7066	. . . . . . . 8 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴))
187	185, 186	mpbiran 710	. . . . . . 7 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)
188	180, 187	sylibr 234	. . . . . 6 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
189	188	adantlr 716	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
190		onss 7733	. . . . . . . 8 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
191	190	adantl 481	. . . . . . 7 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐴 ⊆ On)
192	2	onordi 6431	. . . . . . . 8 ⊢ Ord (cf‘𝐴)
193		fvex 6848	. . . . . . . . . . . . . . . . 17 ⊢ (recs(𝐹)‘𝑦) ∈ V
194	193	sucid 6402	. . . . . . . . . . . . . . . 16 ⊢ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)
195		fveq2 6835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦))
196		suceq 6386	. . . . . . . . . . . . . . . . . . 19 ⊢ ((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
197	195, 196	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
198	197	eliuni 4940	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡))
199	198, 60	eleqtrrdi 2848	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
200	194, 199	mpan2 692	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
201		elun2 4124	. . . . . . . . . . . . . . 15 ⊢ ((recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
202	200, 201	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
203	202	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
204	3	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
205	204, 65	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
206	203, 205	eleqtrrd 2840	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥))
207	22	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥))
208	206, 78, 207	3eltr4d 2852	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ (𝐺‘𝑥))
209	208	expcom 413	. . . . . . . . . 10 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝑦 ∈ 𝑥 → (𝐺‘𝑦) ∈ (𝐺‘𝑥)))
210	209	ralrimiv 3129	. . . . . . . . 9 ⊢ (𝑥 ∈ (cf‘𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥))
211	210	rgen 3054	. . . . . . . 8 ⊢ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)
212		issmo2 8283	. . . . . . . . 9 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → Smo 𝐺))
213	212	com12 32	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
214	192, 211, 213	mp3an23 1456	. . . . . . 7 ⊢ (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
215	191, 188, 214	sylc 65	. . . . . 6 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Smo 𝐺)
216	215	adantlr 716	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺)
217		fveq2 6835	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
218		fveq2 6835	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
219	217, 218	sseq12d 3956	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝑔‘𝑥) ⊆ (𝐺‘𝑥) ↔ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)))
220		ssun1 4119	. . . . . . . . . . 11 ⊢ (𝑔‘𝑥) ⊆ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
221	220, 67	sseqtrrid 3966	. . . . . . . . . 10 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝑔‘𝑥) ⊆ (𝐺‘𝑥))
222	219, 221	vtoclga 3521	. . . . . . . . 9 ⊢ (𝑤 ∈ (cf‘𝐴) → (𝑔‘𝑤) ⊆ (𝐺‘𝑤))
223		sstr 3931	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ (𝑔‘𝑤) ∧ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) → 𝑧 ⊆ (𝐺‘𝑤))
224	223	expcom 413	. . . . . . . . 9 ⊢ ((𝑔‘𝑤) ⊆ (𝐺‘𝑤) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤)))
225	222, 224	syl 17	. . . . . . . 8 ⊢ (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤)))
226	225	reximia 3073	. . . . . . 7 ⊢ (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
227	226	ralimi 3075	. . . . . 6 ⊢ (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
228	227	ad2antlr 728	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
229		fnex 7166	. . . . . . 7 ⊢ ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V)
230	185, 2, 229	mp2an 693	. . . . . 6 ⊢ 𝐺 ∈ V
231		feq1 6641	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴 ↔ 𝐺:(cf‘𝐴)⟶𝐴))
232		smoeq 8284	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺))
233		fveq1 6834	. . . . . . . . . 10 ⊢ (𝑓 = 𝐺 → (𝑓‘𝑤) = (𝐺‘𝑤))
234	233	sseq2d 3955	. . . . . . . . 9 ⊢ (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝐺‘𝑤)))
235	234	rexbidv 3162	. . . . . . . 8 ⊢ (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))
236	235	ralbidv 3161	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))
237	231, 232, 236	3anbi123d 1439	. . . . . 6 ⊢ (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))))
238	230, 237	spcev 3549	. . . . 5 ⊢ ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
239	189, 216, 228, 238	syl3anc 1374	. . . 4 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
240	239	expcom 413	. . 3 ⊢ (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))))
241	240	exlimdv 1935	. 2 ⊢ (𝐴 ∈ On → (∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))))
242	1, 241	mpd 15	1 ⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ∪ cun 3888   ⊆ wss 3890  ∪ ciun 4934   ↦ cmpt 5167  dom cdm 5625   ↾ cres 5627  Ord word 6317  Oncon0 6318  suc csuc 6320  Fun wfun 6487   Fn wfn 6488  ⟶wf 6489  –1-1→wf1 6490  ‘cfv 6493  Smo wsmo 8279  recscrecs 8304  cfccf 9855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-smo 8280  df-recs 8305  df-er 8637  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-card 9857  df-cf 9859  df-acn 9860

This theorem is referenced by:  cfsmo  10187