frecsuclem - Intuitionistic Logic Explorer

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

Theorem frecsuclem 6303

Description: Lemma for frecsuc 6304. 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 6288	. . . . . . . . . . . . 13 ⊢ frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω)
2		frecsuclem.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})
3		recseq 6203	. . . . . . . . . . . . . . 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 4815	. . . . . . . . . . . . 13 ⊢ (recs(𝐺) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω)
6	1, 5	eqtr4i 2163	. . . . . . . . . . . 12 ⊢ frec(𝐹, 𝐴) = (recs(𝐺) ↾ ω)
7	6	fveq1i 5422	. . . . . . . . . . 11 ⊢ (frec(𝐹, 𝐴)‘suc 𝐵) = ((recs(𝐺) ↾ ω)‘suc 𝐵)
8		peano2 4509	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ∈ ω)
9		fvres 5445	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
10	8, 9	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
11	7, 10	syl5eq 2184	. . . . . . . . . 10 ⊢ (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
12	11	3ad2ant3 1004	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
13		eqid 2139	. . . . . . . . . . 11 ⊢ recs(𝐺) = recs(𝐺)
14	2	funmpt2 5162	. . . . . . . . . . . 12 ⊢ Fun 𝐺
15	14	a1i 9	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Fun 𝐺)
16		ordom 4520	. . . . . . . . . . . 12 ⊢ Ord ω
17	16	a1i 9	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Ord ω)
18		vex 2689	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
19	18	a1i 9	. . . . . . . . . . . . 13 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑓 ∈ V)
20		simp2 982	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑦 ∈ ω)
21		simp3 983	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑓:𝑦⟶𝑆)
22		simp11 1011	. . . . . . . . . . . . . . 15 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆)
23		fveq2 5421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → (𝐹‘𝑧) = (𝐹‘𝑤))
24	23	eleq1d 2208	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧) ∈ 𝑆 ↔ (𝐹‘𝑤) ∈ 𝑆))
25	24	cbvralv 2654	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
26	22, 25	sylib 121	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
27		simp12 1012	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝐴 ∈ 𝑆)
28	20, 21, 26, 27	frecabcl 6296	. . . . . . . . . . . . 13 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)
29		dmeq 4739	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
30	29	eqeq1d 2148	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
31		fveq1 5420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑔‘𝑚) = (𝑓‘𝑚))
32	31	fveq2d 5425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → (𝐹‘(𝑔‘𝑚)) = (𝐹‘(𝑓‘𝑚)))
33	32	eleq2d 2209	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))))
34	30, 33	anbi12d 464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))))
35	34	rexbidv 2438	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))))
36	29	eqeq1d 2148	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
37	36	anbi1d 460	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴)))
38	35, 37	orbi12d 782	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))))
39	38	abbidv 2257	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
40	39, 2	fvmptg 5497	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) → (𝐺‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
41	19, 28, 40	syl2anc 408	. . . . . . . . . . . 12 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → (𝐺‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
42	41, 28	eqeltrd 2216	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)
43		limom 4527	. . . . . . . . . . . . . . 15 ⊢ Lim ω
44		limuni 4318	. . . . . . . . . . . . . . 15 ⊢ (Lim ω → ω = ∪ ω)
45	43, 44	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω = ∪ ω
46	45	eleq2i 2206	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω ↔ 𝑦 ∈ ∪ ω)
47		peano2 4509	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
48	46, 47	sylbir 134	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ ω → suc 𝑦 ∈ ω)
49	48	adantl 275	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ∪ ω) → suc 𝑦 ∈ ω)
50	45	eleq2i 2206	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ ω ↔ suc 𝐵 ∈ ∪ ω)
51	8, 50	sylib 121	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ∈ ∪ ω)
52	51	3ad2ant3 1004	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ ∪ ω)
53	13, 15, 17, 42, 49, 52	tfrcldm 6260	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ dom recs(𝐺))
54	13	tfr2a 6218	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ dom recs(𝐺) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
55	53, 54	syl 14	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
56	12, 55	eqtrd 2172	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
57		tfrfun 6217	. . . . . . . . . . 11 ⊢ Fun recs(𝐺)
58	57	a1i 9	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Fun recs(𝐺))
59	8	3ad2ant3 1004	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ ω)
60		resfunexg 5641	. . . . . . . . . 10 ⊢ ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
61	58, 59, 60	syl2anc 408	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
62		frecfcl 6302	. . . . . . . . . . . . 13 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
63	6	feq1i 5265	. . . . . . . . . . . . 13 ⊢ (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (recs(𝐺) ↾ ω):ω⟶𝑆)
64	62, 63	sylib 121	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (recs(𝐺) ↾ ω):ω⟶𝑆)
65	64	3adant3 1001	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ ω):ω⟶𝑆)
66		simp3 983	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → 𝐵 ∈ ω)
67		ordelsuc 4421	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ω ∧ Ord ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
68	16, 67	mpan2 421	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ω → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
69	68	3ad2ant3 1004	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
70	66, 69	mpbid 146	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ⊆ ω)
71		fssres2 5300	. . . . . . . . . . 11 ⊢ (((recs(𝐺) ↾ ω):ω⟶𝑆 ∧ suc 𝐵 ⊆ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆)
72	65, 70, 71	syl2anc 408	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆)
73		simp1 981	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆)
74	73, 25	sylib 121	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
75		simp2 982	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → 𝐴 ∈ 𝑆)
76	59, 72, 74, 75	frecabcl 6296	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)
77		dmeq 4739	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
78	77	eqeq1d 2148	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
79		fveq1 5420	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
80	79	fveq2d 5425	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))
81	80	eleq2d 2209	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))
82	78, 81	anbi12d 464	. . . . . . . . . . . . 13 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
83	82	rexbidv 2438	. . . . . . . . . . . 12 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
84	77	eqeq1d 2148	. . . . . . . . . . . . 13 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅))
85	84	anbi1d 460	. . . . . . . . . . . 12 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))
86	83, 85	orbi12d 782	. . . . . . . . . . 11 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
87	86	abbidv 2257	. . . . . . . . . 10 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
88	87, 2	fvmptg 5497	. . . . . . . . 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 408	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐺‘(recs(𝐺) ↾ suc 𝐵)) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
90	56, 89	eqtrd 2172	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
91	90	abeq2d 2252	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
92		fdm 5278	. . . . . . . . . . . 12 ⊢ ((recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆 → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
93	72, 92	syl 14	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
94		peano3 4510	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ≠ ∅)
95	94	3ad2ant3 1004	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ≠ ∅)
96	93, 95	eqnetrd 2332	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅)
97	96	neneqd 2329	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ¬ dom (recs(𝐺) ↾ suc 𝐵) = ∅)
98	97	intnanrd 917	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))
99		biorf 733	. . . . . . . 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 717	. . . . . . 7 ⊢ (((dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))
102	100, 101	syl6bb 195	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
103	93	eqeq1d 2148	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚))
104		vex 2689	. . . . . . . . . . . 12 ⊢ 𝑚 ∈ V
105		suc11g 4472	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
106	104, 105	mpan2 421	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ω → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
107	106	3ad2ant3 1004	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
108	103, 107	bitrd 187	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝐵 = 𝑚))
109		eqcom 2141	. . . . . . . . 9 ⊢ (𝐵 = 𝑚 ↔ 𝑚 = 𝐵)
110	108, 109	syl6bb 195	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝑚 = 𝐵))
111	110	anbi1d 460	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ((dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
112	111	rexbidv 2438	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
113	91, 102, 112	3bitr2d 215	. . . . 5 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
114		fveq2 5421	. . . . . . . 8 ⊢ (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
115	114	fveq2d 5425	. . . . . . 7 ⊢ (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
116	115	eleq2d 2209	. . . . . 6 ⊢ (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
117	116	ceqsrexbv 2816	. . . . 5 ⊢ (∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
118	113, 117	syl6bb 195	. . . 4 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))))
119	118	3anibar 1149	. . 3 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
120	119	eqrdv 2137	. 2 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
121		sucidg 4338	. . . . . 6 ⊢ (𝐵 ∈ ω → 𝐵 ∈ suc 𝐵)
122		fvres 5445	. . . . . 6 ⊢ (𝐵 ∈ suc 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
123	121, 122	syl 14	. . . . 5 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
124	6	fveq1i 5422	. . . . . 6 ⊢ (frec(𝐹, 𝐴)‘𝐵) = ((recs(𝐺) ↾ ω)‘𝐵)
125		fvres 5445	. . . . . 6 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘𝐵) = (recs(𝐺)‘𝐵))
126	124, 125	syl5eq 2184	. . . . 5 ⊢ (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘𝐵) = (recs(𝐺)‘𝐵))
127	123, 126	eqtr4d 2175	. . . 4 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
128	127	3ad2ant3 1004	. . 3 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
129	128	fveq2d 5425	. 2 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
130	120, 129	eqtrd 2172	1 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 697 ∧ w3a 962 = wceq 1331 ∈ wcel 1480 {cab 2125 ≠ wne 2308 ∀wral 2416 ∃wrex 2417 Vcvv 2686 ⊆ wss 3071 ∅c0 3363 ∪ cuni 3736 ↦ cmpt 3989 Ord word 4284 Lim wlim 4286 suc csuc 4287 ωcom 4504 dom cdm 4539 ↾ cres 4541 Fun wfun 5117 ⟶wf 5119 ‘cfv 5123 recscrecs 6201 freccfrec 6287

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-ral 2421 df-rex 2422 df-reu 2423 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-iord 4288 df-on 4290 df-ilim 4291 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-recs 6202 df-frec 6288

This theorem is referenced by: frecsuc 6304

W3C validator