frecsuclem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > frecsuclem		GIF version

Theorem frecsuclem 6491

Description: Lemma for frecsuc 6492. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.)

**Hypothesis**
Ref	Expression
frecsuclem.g	⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})

**Assertion**
Ref	Expression
frecsuclem	⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))

Distinct variable groups: 𝐴,𝑔,𝑚,𝑥 𝐵,𝑔,𝑚,𝑥 𝑔,𝐹,𝑚,𝑥 𝑧,𝐹,𝑚,𝑥 𝑔,𝐺,𝑚,𝑥 𝑆,𝑚,𝑥,𝑧 Allowed substitution hints: 𝐴(𝑧) 𝐵(𝑧) 𝑆(𝑔) 𝐺(𝑧)

Proof of Theorem frecsuclem Dummy variables 𝑓 𝑤 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-frec 6476	. . . . . . . . . . . . 13 ⊢ frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω)
2		frecsuclem.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})
3		recseq 6391	. . . . . . . . . . . . . . 15 ⊢ (𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) → recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})))
4	2, 3	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ recs(𝐺) = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}))
5	4	reseq1i 4954	. . . . . . . . . . . . 13 ⊢ (recs(𝐺) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω)
6	1, 5	eqtr4i 2228	. . . . . . . . . . . 12 ⊢ frec(𝐹, 𝐴) = (recs(𝐺) ↾ ω)
7	6	fveq1i 5576	. . . . . . . . . . 11 ⊢ (frec(𝐹, 𝐴)‘suc 𝐵) = ((recs(𝐺) ↾ ω)‘suc 𝐵)
8		peano2 4642	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ∈ ω)
9		fvres 5599	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
10	8, 9	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
11	7, 10	eqtrid 2249	. . . . . . . . . 10 ⊢ (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
12	11	3ad2ant3 1022	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
13		eqid 2204	. . . . . . . . . . 11 ⊢ recs(𝐺) = recs(𝐺)
14	2	funmpt2 5309	. . . . . . . . . . . 12 ⊢ Fun 𝐺
15	14	a1i 9	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Fun 𝐺)
16		ordom 4654	. . . . . . . . . . . 12 ⊢ Ord ω
17	16	a1i 9	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Ord ω)
18		vex 2774	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
19	18	a1i 9	. . . . . . . . . . . . 13 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑓 ∈ V)
20		simp2 1000	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑦 ∈ ω)
21		simp3 1001	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑓:𝑦⟶𝑆)
22		simp11 1029	. . . . . . . . . . . . . . 15 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆)
23		fveq2 5575	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → (𝐹‘𝑧) = (𝐹‘𝑤))
24	23	eleq1d 2273	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧) ∈ 𝑆 ↔ (𝐹‘𝑤) ∈ 𝑆))
25	24	cbvralv 2737	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
26	22, 25	sylib 122	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
27		simp12 1030	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝐴 ∈ 𝑆)
28	20, 21, 26, 27	frecabcl 6484	. . . . . . . . . . . . 13 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)
29		dmeq 4877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
30	29	eqeq1d 2213	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
31		fveq1 5574	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑔‘𝑚) = (𝑓‘𝑚))
32	31	fveq2d 5579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → (𝐹‘(𝑔‘𝑚)) = (𝐹‘(𝑓‘𝑚)))
33	32	eleq2d 2274	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))))
34	30, 33	anbi12d 473	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))))
35	34	rexbidv 2506	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))))
36	29	eqeq1d 2213	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
37	36	anbi1d 465	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴)))
38	35, 37	orbi12d 794	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))))
39	38	abbidv 2322	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
40	39, 2	fvmptg 5654	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) → (𝐺‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
41	19, 28, 40	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → (𝐺‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
42	41, 28	eqeltrd 2281	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)
43		limom 4661	. . . . . . . . . . . . . . 15 ⊢ Lim ω
44		limuni 4442	. . . . . . . . . . . . . . 15 ⊢ (Lim ω → ω = ∪ ω)
45	43, 44	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω = ∪ ω
46	45	eleq2i 2271	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω ↔ 𝑦 ∈ ∪ ω)
47		peano2 4642	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
48	46, 47	sylbir 135	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ ω → suc 𝑦 ∈ ω)
49	48	adantl 277	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ∪ ω) → suc 𝑦 ∈ ω)
50	45	eleq2i 2271	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ ω ↔ suc 𝐵 ∈ ∪ ω)
51	8, 50	sylib 122	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ∈ ∪ ω)
52	51	3ad2ant3 1022	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ ∪ ω)
53	13, 15, 17, 42, 49, 52	tfrcldm 6448	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ dom recs(𝐺))
54	13	tfr2a 6406	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ dom recs(𝐺) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
55	53, 54	syl 14	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
56	12, 55	eqtrd 2237	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
57		tfrfun 6405	. . . . . . . . . . 11 ⊢ Fun recs(𝐺)
58	57	a1i 9	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Fun recs(𝐺))
59	8	3ad2ant3 1022	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ ω)
60		resfunexg 5804	. . . . . . . . . 10 ⊢ ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
61	58, 59, 60	syl2anc 411	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
62		frecfcl 6490	. . . . . . . . . . . . 13 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
63	6	feq1i 5417	. . . . . . . . . . . . 13 ⊢ (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (recs(𝐺) ↾ ω):ω⟶𝑆)
64	62, 63	sylib 122	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (recs(𝐺) ↾ ω):ω⟶𝑆)
65	64	3adant3 1019	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ ω):ω⟶𝑆)
66		simp3 1001	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → 𝐵 ∈ ω)
67		ordelsuc 4552	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ω ∧ Ord ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
68	16, 67	mpan2 425	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ω → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
69	68	3ad2ant3 1022	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
70	66, 69	mpbid 147	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ⊆ ω)
71		fssres2 5452	. . . . . . . . . . 11 ⊢ (((recs(𝐺) ↾ ω):ω⟶𝑆 ∧ suc 𝐵 ⊆ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆)
72	65, 70, 71	syl2anc 411	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆)
73		simp1 999	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆)
74	73, 25	sylib 122	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
75		simp2 1000	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → 𝐴 ∈ 𝑆)
76	59, 72, 74, 75	frecabcl 6484	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)
77		dmeq 4877	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
78	77	eqeq1d 2213	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
79		fveq1 5574	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
80	79	fveq2d 5579	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))
81	80	eleq2d 2274	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))
82	78, 81	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
83	82	rexbidv 2506	. . . . . . . . . . . 12 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
84	77	eqeq1d 2213	. . . . . . . . . . . . 13 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅))
85	84	anbi1d 465	. . . . . . . . . . . 12 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))
86	83, 85	orbi12d 794	. . . . . . . . . . 11 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
87	86	abbidv 2322	. . . . . . . . . 10 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
88	87, 2	fvmptg 5654	. . . . . . . . 9 ⊢ (((recs(𝐺) ↾ suc 𝐵) ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
89	61, 76, 88	syl2anc 411	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
90	56, 89	eqtrd 2237	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
91	90	abeq2d 2317	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
92		fdm 5430	. . . . . . . . . . . 12 ⊢ ((recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆 → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
93	72, 92	syl 14	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
94		peano3 4643	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ≠ ∅)
95	94	3ad2ant3 1022	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ≠ ∅)
96	93, 95	eqnetrd 2399	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅)
97	96	neneqd 2396	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ¬ dom (recs(𝐺) ↾ suc 𝐵) = ∅)
98	97	intnanrd 933	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))
99		biorf 745	. . . . . . . 8 ⊢ (¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))))
100	98, 99	syl 14	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))))
101		orcom 729	. . . . . . 7 ⊢ (((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))
102	100, 101	bitrdi 196	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
103	93	eqeq1d 2213	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚))
104		vex 2774	. . . . . . . . . . . 12 ⊢ 𝑚 ∈ V
105		suc11g 4604	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
106	104, 105	mpan2 425	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ω → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
107	106	3ad2ant3 1022	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
108	103, 107	bitrd 188	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝐵 = 𝑚))
109		eqcom 2206	. . . . . . . . 9 ⊢ (𝐵 = 𝑚 ↔ 𝑚 = 𝐵)
110	108, 109	bitrdi 196	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝑚 = 𝐵))
111	110	anbi1d 465	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
112	111	rexbidv 2506	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
113	91, 102, 112	3bitr2d 216	. . . . 5 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
114		fveq2 5575	. . . . . . . 8 ⊢ (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
115	114	fveq2d 5579	. . . . . . 7 ⊢ (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
116	115	eleq2d 2274	. . . . . 6 ⊢ (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
117	116	ceqsrexbv 2903	. . . . 5 ⊢ (∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
118	113, 117	bitrdi 196	. . . 4 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))))
119	118	3anibar 1167	. . 3 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
120	119	eqrdv 2202	. 2 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
121		sucidg 4462	. . . . . 6 ⊢ (𝐵 ∈ ω → 𝐵 ∈ suc 𝐵)
122		fvres 5599	. . . . . 6 ⊢ (𝐵 ∈ suc 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
123	121, 122	syl 14	. . . . 5 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
124	6	fveq1i 5576	. . . . . 6 ⊢ (frec(𝐹, 𝐴)‘𝐵) = ((recs(𝐺) ↾ ω)‘𝐵)
125		fvres 5599	. . . . . 6 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘𝐵) = (recs(𝐺)‘𝐵))
126	124, 125	eqtrid 2249	. . . . 5 ⊢ (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘𝐵) = (recs(𝐺)‘𝐵))
127	123, 126	eqtr4d 2240	. . . 4 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
128	127	3ad2ant3 1022	. . 3 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
129	128	fveq2d 5579	. 2 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
130	120, 129	eqtrd 2237	1 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 ∧ w3a 980 = wceq 1372 ∈ wcel 2175 {cab 2190 ≠ wne 2375 ∀wral 2483 ∃wrex 2484 Vcvv 2771 ⊆ wss 3165 ∅c0 3459 ∪ cuni 3849 ↦ cmpt 4104 Ord word 4408 Lim wlim 4410 suc csuc 4411 ωcom 4637 dom cdm 4674 ↾ cres 4676 Fun wfun 5264 ⟶wf 5266 ‘cfv 5270 recscrecs 6389 freccfrec 6475

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4479 ax-setind 4584 ax-iinf 4635

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-ral 2488 df-rex 2489 df-reu 2490 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4339 df-iord 4412 df-on 4414 df-ilim 4415 df-suc 4417 df-iom 4638 df-xp 4680 df-rel 4681 df-cnv 4682 df-co 4683 df-dm 4684 df-rn 4685 df-res 4686 df-ima 4687 df-iota 5231 df-fun 5272 df-fn 5273 df-f 5274 df-f1 5275 df-fo 5276 df-f1o 5277 df-fv 5278 df-recs 6390 df-frec 6476

This theorem is referenced by: frecsuc 6492

W3C validator