cfsmolem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cfsmolem		Structured version Visualization version GIF version

Theorem cfsmolem 9691

Description: Lemma for cfsmo 9692. (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 9679	. 2 ⊢ (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)))
2		cfon 9676	. . . . . . . . . . . 12 ⊢ (cf‘𝐴) ∈ On
3	2	oneli 6297	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On)
4	3	3ad2ant3 1131	. . . . . . . . . 10 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
5		eleq1w 2895	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴)))
6	5	3anbi3d 1438	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴))))
7		fveq2 6669	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦))
8	7	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝐺‘𝑥) ∈ 𝐴 ↔ (𝐺‘𝑦) ∈ 𝐴))
9	6, 8	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴)))
10		simpl1 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑔:(cf‘𝐴)–1-1→𝐴)
11		simpl2 1188	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
12		ontr1 6236	. . . . . . . . . . . . . . . . . 18 ⊢ ((cf‘𝐴) ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)))
13	2, 12	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))
14	13	ancoms 461	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴))
15	14	3ad2antl3 1183	. . . . . . . . . . . . . . 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 1367	. . . . . . . . . . . . . 14 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
18	17	ralimdva 3177	. . . . . . . . . . . . 13 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴))
19		cfsmolem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))
20	19	fveq1i 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥)
21		fvres 6688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥))
22	20, 21	syl5eq 2868	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥))
23		recsval 8039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥)))
24		recsfnon 8038	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ recs(𝐹) Fn On
25		fnfun 6452	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (recs(𝐹) Fn On → Fun recs(𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun recs(𝐹)
27		vex 3497	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑥 ∈ V
28		resfunexg 6977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V)
29	26, 27, 28	mp2an 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (recs(𝐹) ↾ 𝑥) ∈ V
30		dmeq 5771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥))
31	30	fveq2d 6673	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥)))
32		fveq1 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡))
33		suceq 6255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
35	30, 34	iuneq12d 4946	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡) = ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
36	31, 35	uneq12d 4139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
37		cfsmolem.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)))
38		fvex 6682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V
39	29	dmex 7615	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ dom (recs(𝐹) ↾ 𝑥) ∈ V
40		fvex 6682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
41	40	sucex 7525	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
42	39, 41	iunex 7668	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
43	38, 42	unex 7468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V
44	36, 37, 43	fvmpt 6767	. . . . . . . . . . . . . . . . . . . . . 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	syl6eq 2872	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
47		onss 7504	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
48		fnssres 6469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((recs(𝐹) Fn On ∧ 𝑥 ⊆ On) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
49	24, 47, 48	sylancr 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
50		fndm 6454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥)
51		fveq2 6669	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔‘𝑥))
52		iuneq1 4934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
53		fvres 6688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡))
54		suceq 6255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ 𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
56	55	iuneq2i 4939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)
57		fveq2 6669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡))
58		suceq 6255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
60	59	cbviunv 4964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)
61	56, 60	eqtr4i 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)
62	52, 61	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
63	51, 62	uneq12d 4139	. . . . . . . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
66	3, 65	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
67	22, 66	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
68	67	3ad2ant2 1130	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
69		eloni 6200	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ On → Ord 𝐴)
70	69	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Ord 𝐴)
71	70	3ad2ant1 1129	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → Ord 𝐴)
72		f1f 6574	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:(cf‘𝐴)–1-1→𝐴 → 𝑔:(cf‘𝐴)⟶𝐴)
73	72	ffvelrnda 6850	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴)
74	73	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴)
75	74	3adant3 1128	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝑔‘𝑥) ∈ 𝐴)
76	19	fveq1i 6670	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺‘𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦)
77	13	fvresd 6689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦))
78	76, 77	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
79	78	adantrl 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
80	79	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
81	80	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴))
82		ordsucss 7532	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
83	69, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
84	83	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
85	81, 84	sylbid 242	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
86	85	ralimdva 3177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
87		iunss 4968	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
88	86, 87	syl6ibr 254	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
89	88	3impia 1113	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
90		onelon 6215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On)
91	90	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
92	91	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
93	81, 92	sylbid 242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
94		suceloni 7527	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On)
95	93, 94	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On))
96	95	ralimdva 3177	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On))
97	96	3impia 1113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
98		iunon 7975	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
99	27, 97, 98	sylancr 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
100		simp1 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → 𝐴 ∈ On)
101		onsseleq 6231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
102	99, 100, 101	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
103		idd 24	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
104		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴))
105		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝐴 ∈ On)
106	3	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ On)
107	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
108	107	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
109	78	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
110		fvres 6688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
111	110	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
112	109, 111	eqtr4d 2859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
113	112	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
114	113	ralbidva 3196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (cf‘𝐴) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 ↔ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
115	114	biimpa 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
116		ffnfv 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
117	108, 115, 116	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴)
118		eleq2 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ 𝐴))
119	118	biimpar 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
120	119	adantrl 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
121	120	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
122		onelon 6215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ On)
123	110	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
124		ffvelrn 6848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
125	123, 124	eqeltrrd 2914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴)
126	125, 90	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
127	126	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
128		onsssuc 6277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
129	122, 127, 128	syl2an2r 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
130	129	anassrs 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
131	130	rexbidva 3296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
132		eliun 4922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))
133	131, 132	syl6bbr 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
134	133	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
135	134	3adant2 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
136	121, 135	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
137	136	3expa 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
138	137	anassrs 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
139	138	ralrimiva 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
140	139	expl 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
141	117, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
142	141	imp 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
143		feq1 6494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥⟶𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴))
144		fveq1 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
145	144	sseq2d 3998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓‘𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
146	145	rexbidv 3297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
147	110	sseq2d 3998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ∈ 𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦)))
148	147	rexbiia 3246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
149	146, 148	syl6bb 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
150	149	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
151	143, 150	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))))
152	29, 151	spcev 3606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)))
153	117, 142, 152	syl2an2r 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)))
154		cfflb 9680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
155	154	imp 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) → (cf‘𝐴) ⊆ 𝑥)
156	105, 106, 153, 155	syl21anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥)
157		ontri1 6224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((cf‘𝐴) ∈ On ∧ 𝑥 ∈ On) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
158	2, 3, 157	sylancr 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
159	158	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
160	156, 159	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴))
161	104, 160	pm2.21dd 197	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
162	161	ex 415	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
163	162	expcomd 419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐴 ∈ On → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
164	163	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
165	164	3impib 1112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
166	103, 165	jaod 855	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
167	102, 166	sylbid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
168	89, 167	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
169	168	3adant1l 1172	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
170		ordunel 7541	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝐴 ∧ (𝑔‘𝑥) ∈ 𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
171	71, 75, 169, 170	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
172	68, 171	eqeltrd 2913	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐴)
173	172	3expia 1117	. . . . . . . . . . . . . 14 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴))
174	173	3impa 1106	. . . . . . . . . . . . 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 7570	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴))
178	4, 177	mpcom 38	. . . . . . . . 9 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)
179	178	3expia 1117	. . . . . . . 8 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) ∈ 𝐴))
180	179	ralrimiv 3181	. . . . . . 7 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)
181	2	onssi 7551	. . . . . . . . 9 ⊢ (cf‘𝐴) ⊆ On
182		fnssres 6469	. . . . . . . . . 10 ⊢ ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
183	19	fneq1i 6449	. . . . . . . . . 10 ⊢ (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
184	182, 183	sylibr 236	. . . . . . . . 9 ⊢ ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → 𝐺 Fn (cf‘𝐴))
185	24, 181, 184	mp2an 690	. . . . . . . 8 ⊢ 𝐺 Fn (cf‘𝐴)
186		ffnfv 6881	. . . . . . . 8 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴))
187	185, 186	mpbiran 707	. . . . . . 7 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)
188	180, 187	sylibr 236	. . . . . 6 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
189	188	adantlr 713	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
190		onss 7504	. . . . . . . 8 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
191	190	adantl 484	. . . . . . 7 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐴 ⊆ On)
192	2	onordi 6294	. . . . . . . 8 ⊢ Ord (cf‘𝐴)
193		fvex 6682	. . . . . . . . . . . . . . . . 17 ⊢ (recs(𝐹)‘𝑦) ∈ V
194	193	sucid 6269	. . . . . . . . . . . . . . . 16 ⊢ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)
195		fveq2 6669	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦))
196		suceq 6255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
197	195, 196	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
198	197	eliuni 4924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡))
199	198, 60	eleqtrrdi 2924	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
200	194, 199	mpan2 689	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
201		elun2 4152	. . . . . . . . . . . . . . 15 ⊢ ((recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
202	200, 201	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
203	202	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
204	3	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
205	204, 65	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
206	203, 205	eleqtrrd 2916	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥))
207	22	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥))
208	206, 78, 207	3eltr4d 2928	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ (𝐺‘𝑥))
209	208	expcom 416	. . . . . . . . . 10 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝑦 ∈ 𝑥 → (𝐺‘𝑦) ∈ (𝐺‘𝑥)))
210	209	ralrimiv 3181	. . . . . . . . 9 ⊢ (𝑥 ∈ (cf‘𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥))
211	210	rgen 3148	. . . . . . . 8 ⊢ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)
212		issmo2 7985	. . . . . . . . 9 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → Smo 𝐺))
213	212	com12 32	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
214	192, 211, 213	mp3an23 1449	. . . . . . 7 ⊢ (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
215	191, 188, 214	sylc 65	. . . . . 6 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Smo 𝐺)
216	215	adantlr 713	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺)
217		fveq2 6669	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
218		fveq2 6669	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
219	217, 218	sseq12d 3999	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝑔‘𝑥) ⊆ (𝐺‘𝑥) ↔ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)))
220		ssun1 4147	. . . . . . . . . . 11 ⊢ (𝑔‘𝑥) ⊆ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
221	220, 67	sseqtrrid 4019	. . . . . . . . . 10 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝑔‘𝑥) ⊆ (𝐺‘𝑥))
222	219, 221	vtoclga 3573	. . . . . . . . 9 ⊢ (𝑤 ∈ (cf‘𝐴) → (𝑔‘𝑤) ⊆ (𝐺‘𝑤))
223		sstr 3974	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ (𝑔‘𝑤) ∧ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) → 𝑧 ⊆ (𝐺‘𝑤))
224	223	expcom 416	. . . . . . . . 9 ⊢ ((𝑔‘𝑤) ⊆ (𝐺‘𝑤) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤)))
225	222, 224	syl 17	. . . . . . . 8 ⊢ (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤)))
226	225	reximia 3242	. . . . . . 7 ⊢ (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
227	226	ralimi 3160	. . . . . 6 ⊢ (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
228	227	ad2antlr 725	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
229		fnex 6979	. . . . . . 7 ⊢ ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V)
230	185, 2, 229	mp2an 690	. . . . . 6 ⊢ 𝐺 ∈ V
231		feq1 6494	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴 ↔ 𝐺:(cf‘𝐴)⟶𝐴))
232		smoeq 7986	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺))
233		fveq1 6668	. . . . . . . . . 10 ⊢ (𝑓 = 𝐺 → (𝑓‘𝑤) = (𝐺‘𝑤))
234	233	sseq2d 3998	. . . . . . . . 9 ⊢ (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝐺‘𝑤)))
235	234	rexbidv 3297	. . . . . . . 8 ⊢ (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))
236	235	ralbidv 3197	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))
237	231, 232, 236	3anbi123d 1432	. . . . . 6 ⊢ (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))))
238	230, 237	spcev 3606	. . . . 5 ⊢ ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
239	189, 216, 228, 238	syl3anc 1367	. . . 4 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
240	239	expcom 416	. . 3 ⊢ (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))))
241	240	exlimdv 1930	. 2 ⊢ (𝐴 ∈ On → (∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))))
242	1, 241	mpd 15	1 ⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1533 ∃wex 1776 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ∪ cun 3933 ⊆ wss 3935 ∪ ciun 4918 ↦ cmpt 5145 dom cdm 5554 ↾ cres 5556 Ord word 6189 Oncon0 6190 suc csuc 6192 Fun wfun 6348 Fn wfn 6349 ⟶wf 6350 –1-1→wf1 6351 ‘cfv 6354 Smo wsmo 7981 recscrecs 8006 cfccf 9365

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-rep 5189 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460

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-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 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-int 4876 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-se 5514 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-pred 6147 df-ord 6193 df-on 6194 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-isom 6363 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-1st 7688 df-2nd 7689 df-wrecs 7946 df-smo 7982 df-recs 8007 df-er 8288 df-map 8407 df-en 8509 df-dom 8510 df-sdom 8511 df-card 9367 df-cf 9369 df-acn 9370

This theorem is referenced by: cfsmo 9692

W3C validator