frecsuclem - Intuitionistic Logic Explorer

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

Theorem frecsuclem 6615

Description: Lemma for frecsuc 6616. 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 6600	. . . . . . . . . . . . 13 ⊢ frec(𝐹, 𝐴) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω)
2		frecsuclem.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})
3		recseq 6515	. . . . . . . . . . . . . . 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 5015	. . . . . . . . . . . . 13 ⊢ (recs(𝐺) ↾ ω) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ↾ ω)
6	1, 5	eqtr4i 2255	. . . . . . . . . . . 12 ⊢ frec(𝐹, 𝐴) = (recs(𝐺) ↾ ω)
7	6	fveq1i 5649	. . . . . . . . . . 11 ⊢ (frec(𝐹, 𝐴)‘suc 𝐵) = ((recs(𝐺) ↾ ω)‘suc 𝐵)
8		peano2 4699	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ∈ ω)
9		fvres 5672	. . . . . . . . . . . 12 ⊢ (suc 𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
10	8, 9	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
11	7, 10	eqtrid 2276	. . . . . . . . . 10 ⊢ (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
12	11	3ad2ant3 1047	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (recs(𝐺)‘suc 𝐵))
13		eqid 2231	. . . . . . . . . . 11 ⊢ recs(𝐺) = recs(𝐺)
14	2	funmpt2 5372	. . . . . . . . . . . 12 ⊢ Fun 𝐺
15	14	a1i 9	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Fun 𝐺)
16		ordom 4711	. . . . . . . . . . . 12 ⊢ Ord ω
17	16	a1i 9	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Ord ω)
18		vex 2806	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
19	18	a1i 9	. . . . . . . . . . . . 13 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑓 ∈ V)
20		simp2 1025	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑦 ∈ ω)
21		simp3 1026	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝑓:𝑦⟶𝑆)
22		simp11 1054	. . . . . . . . . . . . . . 15 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆)
23		fveq2 5648	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → (𝐹‘𝑧) = (𝐹‘𝑤))
24	23	eleq1d 2300	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧) ∈ 𝑆 ↔ (𝐹‘𝑤) ∈ 𝑆))
25	24	cbvralv 2768	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
26	22, 25	sylib 122	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
27		simp12 1055	. . . . . . . . . . . . . 14 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → 𝐴 ∈ 𝑆)
28	20, 21, 26, 27	frecabcl 6608	. . . . . . . . . . . . 13 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)
29		dmeq 4937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
30	29	eqeq1d 2240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (dom 𝑔 = suc 𝑚 ↔ dom 𝑓 = suc 𝑚))
31		fveq1 5647	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑔‘𝑚) = (𝑓‘𝑚))
32	31	fveq2d 5652	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → (𝐹‘(𝑔‘𝑚)) = (𝐹‘(𝑓‘𝑚)))
33	32	eleq2d 2301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))))
34	30, 33	anbi12d 473	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))))
35	34	rexbidv 2534	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))))
36	29	eqeq1d 2240	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → (dom 𝑔 = ∅ ↔ dom 𝑓 = ∅))
37	36	anbi1d 465	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴)))
38	35, 37	orbi12d 801	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑓 → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))))
39	38	abbidv 2350	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
40	39, 2	fvmptg 5731	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ V ∧ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) → (𝐺‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
41	19, 28, 40	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → (𝐺‘𝑓) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))})
42	41, 28	eqeltrd 2308	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝑓:𝑦⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)
43		limom 4718	. . . . . . . . . . . . . . 15 ⊢ Lim ω
44		limuni 4499	. . . . . . . . . . . . . . 15 ⊢ (Lim ω → ω = ∪ ω)
45	43, 44	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω = ∪ ω
46	45	eleq2i 2298	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω ↔ 𝑦 ∈ ∪ ω)
47		peano2 4699	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
48	46, 47	sylbir 135	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ ω → suc 𝑦 ∈ ω)
49	48	adantl 277	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ∪ ω) → suc 𝑦 ∈ ω)
50	45	eleq2i 2298	. . . . . . . . . . . . 13 ⊢ (suc 𝐵 ∈ ω ↔ suc 𝐵 ∈ ∪ ω)
51	8, 50	sylib 122	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ∈ ∪ ω)
52	51	3ad2ant3 1047	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ ∪ ω)
53	13, 15, 17, 42, 49, 52	tfrcldm 6572	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ dom recs(𝐺))
54	13	tfr2a 6530	. . . . . . . . . 10 ⊢ (suc 𝐵 ∈ dom recs(𝐺) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
55	53, 54	syl 14	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
56	12, 55	eqtrd 2264	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐺‘(recs(𝐺) ↾ suc 𝐵)))
57		tfrfun 6529	. . . . . . . . . . 11 ⊢ Fun recs(𝐺)
58	57	a1i 9	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → Fun recs(𝐺))
59	8	3ad2ant3 1047	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ∈ ω)
60		resfunexg 5883	. . . . . . . . . 10 ⊢ ((Fun recs(𝐺) ∧ suc 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
61	58, 59, 60	syl2anc 411	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵) ∈ V)
62		frecfcl 6614	. . . . . . . . . . . . 13 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆)
63	6	feq1i 5482	. . . . . . . . . . . . 13 ⊢ (frec(𝐹, 𝐴):ω⟶𝑆 ↔ (recs(𝐺) ↾ ω):ω⟶𝑆)
64	62, 63	sylib 122	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (recs(𝐺) ↾ ω):ω⟶𝑆)
65	64	3adant3 1044	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ ω):ω⟶𝑆)
66		simp3 1026	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → 𝐵 ∈ ω)
67		ordelsuc 4609	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ω ∧ Ord ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
68	16, 67	mpan2 425	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ω → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
69	68	3ad2ant3 1047	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐵 ∈ ω ↔ suc 𝐵 ⊆ ω))
70	66, 69	mpbid 147	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ⊆ ω)
71		fssres2 5522	. . . . . . . . . . 11 ⊢ (((recs(𝐺) ↾ ω):ω⟶𝑆 ∧ suc 𝐵 ⊆ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆)
72	65, 70, 71	syl2anc 411	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆)
73		simp1 1024	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆)
74	73, 25	sylib 122	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ∀𝑤 ∈ 𝑆 (𝐹‘𝑤) ∈ 𝑆)
75		simp2 1025	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → 𝐴 ∈ 𝑆)
76	59, 72, 74, 75	frecabcl 6608	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)
77		dmeq 4937	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → dom 𝑔 = dom (recs(𝐺) ↾ suc 𝐵))
78	77	eqeq1d 2240	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = suc 𝑚 ↔ dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚))
79		fveq1 5647	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑔‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝑚))
80	79	fveq2d 5652	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝐹‘(𝑔‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))
81	80	eleq2d 2301	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (𝑥 ∈ (𝐹‘(𝑔‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))))
82	78, 81	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
83	82	rexbidv 2534	. . . . . . . . . . . 12 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ↔ ∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
84	77	eqeq1d 2240	. . . . . . . . . . . . 13 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → (dom 𝑔 = ∅ ↔ dom (recs(𝐺) ↾ suc 𝐵) = ∅))
85	84	anbi1d 465	. . . . . . . . . . . 12 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)))
86	83, 85	orbi12d 801	. . . . . . . . . . 11 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → ((∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
87	86	abbidv 2350	. . . . . . . . . 10 ⊢ (𝑔 = (recs(𝐺) ↾ suc 𝐵) → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
88	87, 2	fvmptg 5731	. . . . . . . . 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 2264	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = {𝑥 ∣ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))})
91	90	abeq2d 2344	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ∨ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))))
92		fdm 5495	. . . . . . . . . . . 12 ⊢ ((recs(𝐺) ↾ suc 𝐵):suc 𝐵⟶𝑆 → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
93	72, 92	syl 14	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) = suc 𝐵)
94		peano3 4700	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ω → suc 𝐵 ≠ ∅)
95	94	3ad2ant3 1047	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → suc 𝐵 ≠ ∅)
96	93, 95	eqnetrd 2427	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → dom (recs(𝐺) ↾ suc 𝐵) ≠ ∅)
97	96	neneqd 2424	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ¬ dom (recs(𝐺) ↾ suc 𝐵) = ∅)
98	97	intnanrd 940	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ¬ (dom (recs(𝐺) ↾ suc 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴))
99		biorf 752	. . . . . . . 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 736	. . . . . . 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 2240	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ suc 𝐵 = suc 𝑚))
104		vex 2806	. . . . . . . . . . . 12 ⊢ 𝑚 ∈ V
105		suc11g 4661	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ω ∧ 𝑚 ∈ V) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
106	104, 105	mpan2 425	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ω → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
107	106	3ad2ant3 1047	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (suc 𝐵 = suc 𝑚 ↔ 𝐵 = 𝑚))
108	103, 107	bitrd 188	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ↔ 𝐵 = 𝑚))
109		eqcom 2233	. . . . . . . . 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 2534	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (∃𝑚 ∈ ω (dom (recs(𝐺) ↾ suc 𝐵) = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
113	91, 102, 112	3bitr2d 216	. . . . 5 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ ∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)))))
114		fveq2 5648	. . . . . . . 8 ⊢ (𝑚 = 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝑚) = ((recs(𝐺) ↾ suc 𝐵)‘𝐵))
115	114	fveq2d 5652	. . . . . . 7 ⊢ (𝑚 = 𝐵 → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
116	115	eleq2d 2301	. . . . . 6 ⊢ (𝑚 = 𝐵 → (𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚)) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
117	116	ceqsrexbv 2938	. . . . 5 ⊢ (∃𝑚 ∈ ω (𝑚 = 𝐵 ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝑚))) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
118	113, 117	bitrdi 196	. . . 4 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ (𝐵 ∈ ω ∧ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))))
119	118	3anibar 1192	. . 3 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝑥 ∈ (frec(𝐹, 𝐴)‘suc 𝐵) ↔ 𝑥 ∈ (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵))))
120	119	eqrdv 2229	. 2 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)))
121		sucidg 4519	. . . . . 6 ⊢ (𝐵 ∈ ω → 𝐵 ∈ suc 𝐵)
122		fvres 5672	. . . . . 6 ⊢ (𝐵 ∈ suc 𝐵 → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
123	121, 122	syl 14	. . . . 5 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (recs(𝐺)‘𝐵))
124	6	fveq1i 5649	. . . . . 6 ⊢ (frec(𝐹, 𝐴)‘𝐵) = ((recs(𝐺) ↾ ω)‘𝐵)
125		fvres 5672	. . . . . 6 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ ω)‘𝐵) = (recs(𝐺)‘𝐵))
126	124, 125	eqtrid 2276	. . . . 5 ⊢ (𝐵 ∈ ω → (frec(𝐹, 𝐴)‘𝐵) = (recs(𝐺)‘𝐵))
127	123, 126	eqtr4d 2267	. . . 4 ⊢ (𝐵 ∈ ω → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
128	127	3ad2ant3 1047	. . 3 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → ((recs(𝐺) ↾ suc 𝐵)‘𝐵) = (frec(𝐹, 𝐴)‘𝐵))
129	128	fveq2d 5652	. 2 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (𝐹‘((recs(𝐺) ↾ suc 𝐵)‘𝐵)) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))
130	120, 129	eqtrd 2264	1 ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 ∧ w3a 1005 = wceq 1398 ∈ wcel 2202 {cab 2217 ≠ wne 2403 ∀wral 2511 ∃wrex 2512 Vcvv 2803 ⊆ wss 3201 ∅c0 3496 ∪ cuni 3898 ↦ cmpt 4155 Ord word 4465 Lim wlim 4467 suc csuc 4468 ωcom 4694 dom cdm 4731 ↾ cres 4733 Fun wfun 5327 ⟶wf 5329 ‘cfv 5333 recscrecs 6513 freccfrec 6599

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-ral 2516 df-rex 2517 df-reu 2518 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-recs 6514 df-frec 6600

This theorem is referenced by: frecsuc 6616

W3C validator