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 9681

Description: Lemma for cfsmo 9682. (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 9669	. 2 ⊢ (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)))
2		cfon 9666	. . . . . . . . . . . 12 ⊢ (cf‘𝐴) ∈ On
3	2	oneli 6266	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On)
4	3	3ad2ant3 1132	. . . . . . . . . 10 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
5		eleq1w 2872	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴)))
6	5	3anbi3d 1439	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴))))
7		fveq2 6645	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦))
8	7	eleq1d 2874	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝐺‘𝑥) ∈ 𝐴 ↔ (𝐺‘𝑦) ∈ 𝐴))
9	6, 8	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴)))
10		simpl1 1188	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑔:(cf‘𝐴)–1-1→𝐴)
11		simpl2 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On)
12		ontr1 6205	. . . . . . . . . . . . . . . . . 18 ⊢ ((cf‘𝐴) ∈ On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)))
13	2, 12	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))
14	13	ancoms 462	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴))
15	14	3ad2antl3 1184	. . . . . . . . . . . . . . 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 1368	. . . . . . . . . . . . . 14 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
18	17	ralimdva 3144	. . . . . . . . . . . . 13 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴))
19		cfsmolem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))
20	19	fveq1i 6646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥)
21		fvres 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥))
22	20, 21	syl5eq 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥))
23		recsval 8023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥)))
24		recsfnon 8022	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ recs(𝐹) Fn On
25		fnfun 6423	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (recs(𝐹) Fn On → Fun recs(𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun recs(𝐹)
27		vex 3444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑥 ∈ V
28		resfunexg 6955	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V)
29	26, 27, 28	mp2an 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (recs(𝐹) ↾ 𝑥) ∈ V
30		dmeq 5736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥))
31	30	fveq2d 6649	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥)))
32		fveq1 6644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡))
33		suceq 6224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
35	30, 34	iuneq12d 4909	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡) = ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
36	31, 35	uneq12d 4091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
37		cfsmolem.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)))
38		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V
39	29	dmex 7598	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ dom (recs(𝐹) ↾ 𝑥) ∈ V
40		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
41	40	sucex 7506	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
42	39, 41	iunex 7651	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
43	38, 42	unex 7449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V
44	36, 37, 43	fvmpt 6745	. . . . . . . . . . . . . . . . . . . . . 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 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
47		onss 7485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
48		fnssres 6442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((recs(𝐹) Fn On ∧ 𝑥 ⊆ On) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
49	24, 47, 48	sylancr 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
50		fndm 6425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥)
51		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔‘𝑥))
52		iuneq1 4897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
53		fvres 6664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡))
54		suceq 6224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ 𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
56	55	iuneq2i 4902	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)
57		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡))
58		suceq 6224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
60	59	cbviunv 4927	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)
61	56, 60	eqtr4i 2824	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)
62	52, 61	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
63	51, 62	uneq12d 4091	. . . . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
66	3, 65	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
67	22, 66	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
68	67	3ad2ant2 1131	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
69		eloni 6169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ On → Ord 𝐴)
70	69	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Ord 𝐴)
71	70	3ad2ant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → Ord 𝐴)
72		f1f 6549	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:(cf‘𝐴)–1-1→𝐴 → 𝑔:(cf‘𝐴)⟶𝐴)
73	72	ffvelrnda 6828	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴)
74	73	adantlr 714	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴)
75	74	3adant3 1129	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝑔‘𝑥) ∈ 𝐴)
76	19	fveq1i 6646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺‘𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦)
77	13	fvresd 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦))
78	76, 77	syl5eq 2845	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
79	78	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
80	79	ancoms 462	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
81	80	eleq1d 2874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴))
82		ordsucss 7513	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
83	69, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
84	83	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
85	81, 84	sylbid 243	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
86	85	ralimdva 3144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
87		iunss 4932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
88	86, 87	syl6ibr 255	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
89	88	3impia 1114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
90		onelon 6184	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On)
91	90	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
92	91	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
93	81, 92	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
94		suceloni 7508	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On)
95	93, 94	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On))
96	95	ralimdva 3144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On))
97	96	3impia 1114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
98		iunon 7959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
99	27, 97, 98	sylancr 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
100		simp1 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → 𝐴 ∈ On)
101		onsseleq 6200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
102	99, 100, 101	syl2anc 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
103		idd 24	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
104		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴))
105		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝐴 ∈ On)
106	3	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ On)
107	3, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
108	107	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
109	78	ancoms 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦))
110		fvres 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
111	110	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
112	109, 111	eqtr4d 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
113	112	eleq1d 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
114	113	ralbidva 3161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (cf‘𝐴) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 ↔ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
115	114	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
116		ffnfv 6859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
117	108, 115, 116	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴)
118		eleq2 2878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ 𝐴))
119	118	biimpar 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
120	119	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
121	120	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
122		onelon 6184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ On)
123	110	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
124		ffvelrn 6826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
125	123, 124	eqeltrrd 2891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴)
126	125, 90	sylan2 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
127	126	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
128		onsssuc 6246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
129	122, 127, 128	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
130	129	anassrs 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
131	130	rexbidva 3255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
132		eliun 4885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))
133	131, 132	syl6bbr 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
134	133	ancoms 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
135	134	3adant2 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
136	121, 135	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
137	136	3expa 1115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
138	137	anassrs 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
139	138	ralrimiva 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
140	139	expl 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
141	117, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
142	141	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
143		feq1 6468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥⟶𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴))
144		fveq1 6644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
145	144	sseq2d 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓‘𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
146	145	rexbidv 3256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
147	110	sseq2d 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 ∈ 𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦)))
148	147	rexbiia 3209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
149	146, 148	syl6bb 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
150	149	ralbidv 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
151	143, 150	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))))
152	29, 151	spcev 3555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)))
153	117, 142, 152	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)))
154		cfflb 9670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ 𝑥))
155	154	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) → (cf‘𝐴) ⊆ 𝑥)
156	105, 106, 153, 155	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥)
157		ontri1 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((cf‘𝐴) ∈ On ∧ 𝑥 ∈ On) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
158	2, 3, 157	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
159	158	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
160	156, 159	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴))
161	104, 160	pm2.21dd 198	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
162	161	ex 416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
163	162	expcomd 420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐴 ∈ On → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
164	163	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
165	164	3impib 1113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
166	103, 165	jaod 856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
167	102, 166	sylbid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
168	89, 167	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
169	168	3adant1l 1173	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
170		ordunel 7522	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝐴 ∧ (𝑔‘𝑥) ∈ 𝐴 ∧ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
171	71, 75, 169, 170	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
172	68, 171	eqeltrd 2890	. . . . . . . . . . . . . . 15 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐴)
173	172	3expia 1118	. . . . . . . . . . . . . 14 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴))
174	173	3impa 1107	. . . . . . . . . . . . 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 7551	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴))
178	4, 177	mpcom 38	. . . . . . . . 9 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)
179	178	3expia 1118	. . . . . . . 8 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) ∈ 𝐴))
180	179	ralrimiv 3148	. . . . . . 7 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)
181	2	onssi 7532	. . . . . . . . 9 ⊢ (cf‘𝐴) ⊆ On
182		fnssres 6442	. . . . . . . . . 10 ⊢ ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
183	19	fneq1i 6420	. . . . . . . . . 10 ⊢ (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
184	182, 183	sylibr 237	. . . . . . . . 9 ⊢ ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → 𝐺 Fn (cf‘𝐴))
185	24, 181, 184	mp2an 691	. . . . . . . 8 ⊢ 𝐺 Fn (cf‘𝐴)
186		ffnfv 6859	. . . . . . . 8 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴))
187	185, 186	mpbiran 708	. . . . . . 7 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)
188	180, 187	sylibr 237	. . . . . 6 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
189	188	adantlr 714	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
190		onss 7485	. . . . . . . 8 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
191	190	adantl 485	. . . . . . 7 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐴 ⊆ On)
192	2	onordi 6263	. . . . . . . 8 ⊢ Ord (cf‘𝐴)
193		fvex 6658	. . . . . . . . . . . . . . . . 17 ⊢ (recs(𝐹)‘𝑦) ∈ V
194	193	sucid 6238	. . . . . . . . . . . . . . . 16 ⊢ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)
195		fveq2 6645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦))
196		suceq 6224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
197	195, 196	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
198	197	eliuni 4887	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡))
199	198, 60	eleqtrrdi 2901	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
200	194, 199	mpan2 690	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
201		elun2 4104	. . . . . . . . . . . . . . 15 ⊢ ((recs(𝐹)‘𝑦) ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
202	200, 201	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
203	202	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
204	3	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
205	204, 65	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)))
206	203, 205	eleqtrrd 2893	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥))
207	22	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥))
208	206, 78, 207	3eltr4d 2905	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ (𝐺‘𝑥))
209	208	expcom 417	. . . . . . . . . 10 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝑦 ∈ 𝑥 → (𝐺‘𝑦) ∈ (𝐺‘𝑥)))
210	209	ralrimiv 3148	. . . . . . . . 9 ⊢ (𝑥 ∈ (cf‘𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥))
211	210	rgen 3116	. . . . . . . 8 ⊢ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)
212		issmo2 7969	. . . . . . . . 9 ⊢ (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → Smo 𝐺))
213	212	com12 32	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
214	192, 211, 213	mp3an23 1450	. . . . . . 7 ⊢ (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
215	191, 188, 214	sylc 65	. . . . . 6 ⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Smo 𝐺)
216	215	adantlr 714	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺)
217		fveq2 6645	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
218		fveq2 6645	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
219	217, 218	sseq12d 3948	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝑔‘𝑥) ⊆ (𝐺‘𝑥) ↔ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)))
220		ssun1 4099	. . . . . . . . . . 11 ⊢ (𝑔‘𝑥) ⊆ ((𝑔‘𝑥) ∪ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))
221	220, 67	sseqtrrid 3968	. . . . . . . . . 10 ⊢ (𝑥 ∈ (cf‘𝐴) → (𝑔‘𝑥) ⊆ (𝐺‘𝑥))
222	219, 221	vtoclga 3522	. . . . . . . . 9 ⊢ (𝑤 ∈ (cf‘𝐴) → (𝑔‘𝑤) ⊆ (𝐺‘𝑤))
223		sstr 3923	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ (𝑔‘𝑤) ∧ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) → 𝑧 ⊆ (𝐺‘𝑤))
224	223	expcom 417	. . . . . . . . 9 ⊢ ((𝑔‘𝑤) ⊆ (𝐺‘𝑤) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤)))
225	222, 224	syl 17	. . . . . . . 8 ⊢ (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤)))
226	225	reximia 3205	. . . . . . 7 ⊢ (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
227	226	ralimi 3128	. . . . . 6 ⊢ (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
228	227	ad2antlr 726	. . . . 5 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))
229		fnex 6957	. . . . . . 7 ⊢ ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V)
230	185, 2, 229	mp2an 691	. . . . . 6 ⊢ 𝐺 ∈ V
231		feq1 6468	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴 ↔ 𝐺:(cf‘𝐴)⟶𝐴))
232		smoeq 7970	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺))
233		fveq1 6644	. . . . . . . . . 10 ⊢ (𝑓 = 𝐺 → (𝑓‘𝑤) = (𝐺‘𝑤))
234	233	sseq2d 3947	. . . . . . . . 9 ⊢ (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝐺‘𝑤)))
235	234	rexbidv 3256	. . . . . . . 8 ⊢ (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))
236	235	ralbidv 3162	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))
237	231, 232, 236	3anbi123d 1433	. . . . . 6 ⊢ (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))))
238	230, 237	spcev 3555	. . . . 5 ⊢ ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
239	189, 216, 228, 238	syl3anc 1368	. . . 4 ⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
240	239	expcom 417	. . 3 ⊢ (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))))
241	240	exlimdv 1934	. 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 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 Vcvv 3441 ∪ cun 3879 ⊆ wss 3881 ∪ ciun 4881 ↦ cmpt 5110 dom cdm 5519 ↾ cres 5521 Ord word 6158 Oncon0 6159 suc csuc 6161 Fun wfun 6318 Fn wfn 6319 ⟶wf 6320 –1-1→wf1 6321 ‘cfv 6324 Smo wsmo 7965 recscrecs 7990 cfccf 9350

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-smo 7966 df-recs 7991 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-card 9352 df-cf 9354 df-acn 9355

This theorem is referenced by: cfsmo 9682

W3C validator