Theorem dfrdg2 36151

Description: Alternate definition of the recursive function generator when 𝐼 is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

Assertion

Ref	Expression
dfrdg2	⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})

Distinct variable groups:   𝑓,𝐹,𝑥,𝑦   𝑓,𝐼,𝑥,𝑦

Allowed substitution hints:   𝑉(𝑥,𝑦,𝑓)

Proof of Theorem dfrdg2

Dummy variables 𝑔 𝑖 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rdgeq2 8387	. . 3 ⊢ (𝑖 = 𝐼 → rec(𝐹, 𝑖) = rec(𝐹, 𝐼))
2		ifeq1 4487	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
3	2	eqeq2d 2776	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ((𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
4	3	ralbidv 3188	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
5	4	anbi2d 641	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
6	5	rexbidv 3189	. . . . 5 ⊢ (𝑖 = 𝐼 → (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
7	6	abbidv 2831	. . . 4 ⊢ (𝑖 = 𝐼 → {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
8	7	unieqd 4880	. . 3 ⊢ (𝑖 = 𝐼 → ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
9	1, 8	eqeq12d 2781	. 2 ⊢ (𝑖 = 𝐼 → (rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} ↔ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}))
10		df-rdg 8385	. . 3 ⊢ rec(𝐹, 𝑖) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))))
11		dfrecs3 8347	. . 3 ⊢ recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))}
12		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑓 ∈ V
13	12	resex 6018	. . . . . . . . . . . 12 ⊢ (𝑓 ↾ 𝑦) ∈ V
14		eqeq1 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ (𝑓 ↾ 𝑦) = ∅))
15		relres 5994	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑓 ↾ 𝑦)
16		reldm0 5908	. . . . . . . . . . . . . . . 16 ⊢ (Rel (𝑓 ↾ 𝑦) → ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅))
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅)
18	14, 17	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅))
19		dmeq 5883	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → dom 𝑔 = dom (𝑓 ↾ 𝑦))
20		limeq 6361	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑔 = dom (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦)))
21	19, 20	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦)))
22		rneq 5916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = ran (𝑓 ↾ 𝑦))
23		df-ima 5664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 “ 𝑦) = ran (𝑓 ↾ 𝑦)
24	22, 23	eqtr4di 2818	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = (𝑓 “ 𝑦))
25	24	unieqd 4880	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ ran 𝑔 = ∪ (𝑓 “ 𝑦))
26		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → 𝑔 = (𝑓 ↾ 𝑦))
27	19	unieqd 4880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ dom 𝑔 = ∪ dom (𝑓 ↾ 𝑦))
28	26, 27	fveq12d 6878	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔‘∪ dom 𝑔) = ((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))
29	28	fveq2d 6875	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝐹‘(𝑔‘∪ dom 𝑔)) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))
30	21, 25, 29	ifbieq12d 4512	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))) = if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))))
31	18, 30	ifbieq2d 4510	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))))
32		eqid 2765	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))
33		vex 3461	. . . . . . . . . . . . . 14 ⊢ 𝑖 ∈ V
34		imaexg 7898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ V → (𝑓 “ 𝑦) ∈ V)
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 “ 𝑦) ∈ V
36	35	uniex 7728	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑓 “ 𝑦) ∈ V
37		fvex 6884	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))) ∈ V
38	36, 37	ifex 4534	. . . . . . . . . . . . . 14 ⊢ if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))) ∈ V
39	33, 38	ifex 4534	. . . . . . . . . . . . 13 ⊢ if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) ∈ V
40	31, 32, 39	fvmpt 6979	. . . . . . . . . . . 12 ⊢ ((𝑓 ↾ 𝑦) ∈ V → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))))
41	13, 40	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))))
42		dmres 6001	. . . . . . . . . . . . 13 ⊢ dom (𝑓 ↾ 𝑦) = (𝑦 ∩ dom 𝑓)
43		onelss 6392	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ On → (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥))
44	43	imp 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥)
45	44	3adant2 1147	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥)
46		fndm 6628	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥)
47	46	3ad2ant2 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom 𝑓 = 𝑥)
48	45, 47	sseqtrrd 3976	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ dom 𝑓)
49		dfss2 3925	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ dom 𝑓 ↔ (𝑦 ∩ dom 𝑓) = 𝑦)
50	48, 49	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ dom 𝑓) = 𝑦)
51	42, 50	eqtrid 2812	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom (𝑓 ↾ 𝑦) = 𝑦)
52		eqeq1 2769	. . . . . . . . . . . . . 14 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (dom (𝑓 ↾ 𝑦) = ∅ ↔ 𝑦 = ∅))
53		limeq 6361	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (Lim dom (𝑓 ↾ 𝑦) ↔ Lim 𝑦))
54		unieq 4878	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → ∪ dom (𝑓 ↾ 𝑦) = ∪ 𝑦)
55	54	fveq2d 6875	. . . . . . . . . . . . . . . 16 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → ((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)) = ((𝑓 ↾ 𝑦)‘∪ 𝑦))
56	55	fveq2d 6875	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))
57	53, 56	ifbieq2d 4510	. . . . . . . . . . . . . 14 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))))
58	52, 57	ifbieq2d 4510	. . . . . . . . . . . . 13 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))))
59		onelon 6374	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
60		eloni 6359	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → Ord 𝑦)
61	59, 60	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
62	61	3adant2 1147	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
63		ordzsl 7829	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝑦 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦))
64		iftrue 4489	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = 𝑖)
65		iftrue 4489	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = 𝑖)
66	64, 65	eqtr4d 2803	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
67		vex 3461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
68	67	sucid 6434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ suc 𝑧
69		fvres 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ suc 𝑧 → ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧))
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧)
71		eloni 6359	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → Ord 𝑧)
72		ordunisuc 7816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑧 → ∪ suc 𝑧 = 𝑧)
73	71, 72	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ On → ∪ suc 𝑧 = 𝑧)
74	73	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧) = ((𝑓 ↾ suc 𝑧)‘𝑧))
75	73	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑓‘∪ suc 𝑧) = (𝑓‘𝑧))
76	70, 74, 75	3eqtr4a 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧) = (𝑓‘∪ suc 𝑧))
77	76	fveq2d 6875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ On → (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
78		nsuceq0 6435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑧 ≠ ∅
79	78	neii 2962	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ suc 𝑧 = ∅
80	79	iffalsei 4493	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))
81		nlimsucg 7826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ V → ¬ Lim suc 𝑧)
82		iffalse 4492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))
83	67, 81, 82	mp2b 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))
84	80, 83	eqtri 2788	. . . . . . . . . . . . . . . . . . 19 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))
85	79	iffalsei 4493	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))
86		iffalse 4492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)))
87	67, 81, 86	mp2b 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))
88	85, 87	eqtri 2788	. . . . . . . . . . . . . . . . . . 19 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧))
89	77, 84, 88	3eqtr4g 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
90		eqeq1 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
91		limeq 6361	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
92		reseq2 5963	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = suc 𝑧 → (𝑓 ↾ 𝑦) = (𝑓 ↾ suc 𝑧))
93		unieq 4878	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧)
94	92, 93	fveq12d 6878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = suc 𝑧 → ((𝑓 ↾ 𝑦)‘∪ 𝑦) = ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))
95	94	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))
96	91, 95	ifbieq2d 4510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))))
97	90, 96	ifbieq2d 4510	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))))
98	93	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧))
99	98	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
100	91, 99	ifbieq2d 4510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))
101	90, 100	ifbieq2d 4510	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
102	97, 101	eqeq12d 2781	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = suc 𝑧 → (if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))))
103	89, 102	syl5ibrcom 250	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ On → (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
104	103	rexlimiv 3159	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
105		iftrue 4489	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
106		df-lim 6354	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Lim 𝑦 ↔ (Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦))
107	106	simp2bi 1162	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑦 → 𝑦 ≠ ∅)
108	107	neneqd 2965	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑦 → ¬ 𝑦 = ∅)
109	108	iffalsed 4494	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))))
110		iftrue 4489	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
111	105, 109, 110	3eqtr4d 2810	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
112	108	iffalsed 4494	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
113	111, 112	eqtr4d 2803	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
114	66, 104, 113	3jaoi 1450	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
115	63, 114	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
116	62, 115	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
117	58, 116	sylan9eqr 2822	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) ∧ dom (𝑓 ↾ 𝑦) = 𝑦) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
118	51, 117	mpdan 699	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
119	41, 118	eqtrid 2812	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
120	119	eqeq2d 2776	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
121	120	3expa 1134	. . . . . . . 8 ⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
122	121	ralbidva 3186	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
123	122	pm5.32da 589	. . . . . 6 ⊢ (𝑥 ∈ On → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
124	123	rexbiia 3110	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
125	124	abbii 2832	. . . 4 ⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
126	125	unieqi 4879	. . 3 ⊢ ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
127	10, 11, 126	3eqtri 2792	. 2 ⊢ rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
128	9, 127	vtoclg 3525	1 ⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ w3o 1100   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  {cab 2743   ≠ wne 2960  ∀wral 3079  ∃wrex 3089  Vcvv 3457   ∩ cin 3906   ⊆ wss 3907  ∅c0 4288  ifcif 4483  ∪ cuni 4867   ↦ cmpt 5185  dom cdm 5651  ran crn 5652   ↾ cres 5653   “ cima 5654  Rel wrel 5656  Ord word 6348  Oncon0 6349  Lim wlim 6350  suc csuc 6351   Fn wfn 6520  ‘cfv 6525  recscrecs 8345  reccrdg 8384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fo 6531  df-fv 6533  df-ov 7403  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385

This theorem is referenced by:  dfrdg3  36152