Theorem dfrdg2 34798

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 8412	. . 3 ⊢ (𝑖 = 𝐼 → rec(𝐹, 𝑖) = rec(𝐹, 𝐼))
2		ifeq1 4533	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
3	2	eqeq2d 2744	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ((𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
4	3	ralbidv 3178	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
5	4	anbi2d 630	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
6	5	rexbidv 3179	. . . . 5 ⊢ (𝑖 = 𝐼 → (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
7	6	abbidv 2802	. . . 4 ⊢ (𝑖 = 𝐼 → {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
8	7	unieqd 4923	. . 3 ⊢ (𝑖 = 𝐼 → ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
9	1, 8	eqeq12d 2749	. 2 ⊢ (𝑖 = 𝐼 → (rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} ↔ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}))
10		df-rdg 8410	. . 3 ⊢ rec(𝐹, 𝑖) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))))
11		dfrecs3 8372	. . 3 ⊢ recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))}
12		vex 3479	. . . . . . . . . . . . 13 ⊢ 𝑓 ∈ V
13	12	resex 6030	. . . . . . . . . . . 12 ⊢ (𝑓 ↾ 𝑦) ∈ V
14		eqeq1 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ (𝑓 ↾ 𝑦) = ∅))
15		relres 6011	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑓 ↾ 𝑦)
16		reldm0 5928	. . . . . . . . . . . . . . . 16 ⊢ (Rel (𝑓 ↾ 𝑦) → ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅))
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅)
18	14, 17	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅))
19		dmeq 5904	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → dom 𝑔 = dom (𝑓 ↾ 𝑦))
20		limeq 6377	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑔 = dom (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦)))
21	19, 20	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦)))
22		rneq 5936	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = ran (𝑓 ↾ 𝑦))
23		df-ima 5690	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 “ 𝑦) = ran (𝑓 ↾ 𝑦)
24	22, 23	eqtr4di 2791	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = (𝑓 “ 𝑦))
25	24	unieqd 4923	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ ran 𝑔 = ∪ (𝑓 “ 𝑦))
26		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → 𝑔 = (𝑓 ↾ 𝑦))
27	19	unieqd 4923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ dom 𝑔 = ∪ dom (𝑓 ↾ 𝑦))
28	26, 27	fveq12d 6899	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔‘∪ dom 𝑔) = ((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))
29	28	fveq2d 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝐹‘(𝑔‘∪ dom 𝑔)) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))
30	21, 25, 29	ifbieq12d 4557	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))) = if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))))
31	18, 30	ifbieq2d 4555	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))))
32		eqid 2733	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))
33		vex 3479	. . . . . . . . . . . . . 14 ⊢ 𝑖 ∈ V
34		imaexg 7906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ V → (𝑓 “ 𝑦) ∈ V)
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 “ 𝑦) ∈ V
36	35	uniex 7731	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑓 “ 𝑦) ∈ V
37		fvex 6905	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))) ∈ V
38	36, 37	ifex 4579	. . . . . . . . . . . . . 14 ⊢ if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))) ∈ V
39	33, 38	ifex 4579	. . . . . . . . . . . . 13 ⊢ if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) ∈ V
40	31, 32, 39	fvmpt 6999	. . . . . . . . . . . 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 6004	. . . . . . . . . . . . 13 ⊢ dom (𝑓 ↾ 𝑦) = (𝑦 ∩ dom 𝑓)
43		onelss 6407	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ On → (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥))
44	43	imp 408	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥)
45	44	3adant2 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥)
46		fndm 6653	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥)
47	46	3ad2ant2 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom 𝑓 = 𝑥)
48	45, 47	sseqtrrd 4024	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ dom 𝑓)
49		df-ss 3966	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ dom 𝑓 ↔ (𝑦 ∩ dom 𝑓) = 𝑦)
50	48, 49	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ dom 𝑓) = 𝑦)
51	42, 50	eqtrid 2785	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom (𝑓 ↾ 𝑦) = 𝑦)
52		eqeq1 2737	. . . . . . . . . . . . . 14 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (dom (𝑓 ↾ 𝑦) = ∅ ↔ 𝑦 = ∅))
53		limeq 6377	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (Lim dom (𝑓 ↾ 𝑦) ↔ Lim 𝑦))
54		unieq 4920	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → ∪ dom (𝑓 ↾ 𝑦) = ∪ 𝑦)
55	54	fveq2d 6896	. . . . . . . . . . . . . . . 16 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → ((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)) = ((𝑓 ↾ 𝑦)‘∪ 𝑦))
56	55	fveq2d 6896	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))
57	53, 56	ifbieq2d 4555	. . . . . . . . . . . . . 14 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))))
58	52, 57	ifbieq2d 4555	. . . . . . . . . . . . 13 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))))
59		onelon 6390	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
60		eloni 6375	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → Ord 𝑦)
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
62	61	3adant2 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
63		ordzsl 7834	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝑦 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦))
64		iftrue 4535	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = 𝑖)
65		iftrue 4535	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = 𝑖)
66	64, 65	eqtr4d 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
67		vex 3479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
68	67	sucid 6447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ suc 𝑧
69		fvres 6911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ suc 𝑧 → ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧))
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧)
71		eloni 6375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → Ord 𝑧)
72		ordunisuc 7820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑧 → ∪ suc 𝑧 = 𝑧)
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ On → ∪ suc 𝑧 = 𝑧)
74	73	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧) = ((𝑓 ↾ suc 𝑧)‘𝑧))
75	73	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑓‘∪ suc 𝑧) = (𝑓‘𝑧))
76	70, 74, 75	3eqtr4a 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧) = (𝑓‘∪ suc 𝑧))
77	76	fveq2d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ On → (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
78		nsuceq0 6448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑧 ≠ ∅
79	78	neii 2943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ suc 𝑧 = ∅
80	79	iffalsei 4539	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))
81		nlimsucg 7831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ V → ¬ Lim suc 𝑧)
82		iffalse 4538	. . . . . . . . . . . . . . . . . . . . 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 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))
85	79	iffalsei 4539	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))
86		iffalse 4538	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)))
87	67, 81, 86	mp2b 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))
88	85, 87	eqtri 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧))
89	77, 84, 88	3eqtr4g 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
90		eqeq1 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
91		limeq 6377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
92		reseq2 5977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = suc 𝑧 → (𝑓 ↾ 𝑦) = (𝑓 ↾ suc 𝑧))
93		unieq 4920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧)
94	92, 93	fveq12d 6899	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = suc 𝑧 → ((𝑓 ↾ 𝑦)‘∪ 𝑦) = ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))
95	94	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))
96	91, 95	ifbieq2d 4555	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))))
97	90, 96	ifbieq2d 4555	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))))
98	93	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧))
99	98	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
100	91, 99	ifbieq2d 4555	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))
101	90, 100	ifbieq2d 4555	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
102	97, 101	eqeq12d 2749	. . . . . . . . . . . . . . . . . 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 246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ On → (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
104	103	rexlimiv 3149	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
105		iftrue 4535	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
106		df-lim 6370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Lim 𝑦 ↔ (Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦))
107	106	simp2bi 1147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑦 → 𝑦 ≠ ∅)
108	107	neneqd 2946	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑦 → ¬ 𝑦 = ∅)
109	108	iffalsed 4540	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))))
110		iftrue 4535	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
111	105, 109, 110	3eqtr4d 2783	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
112	108	iffalsed 4540	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
113	111, 112	eqtr4d 2776	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
114	66, 104, 113	3jaoi 1428	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
115	63, 114	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
116	62, 115	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
117	58, 116	sylan9eqr 2795	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) ∧ dom (𝑓 ↾ 𝑦) = 𝑦) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
118	51, 117	mpdan 686	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
119	41, 118	eqtrid 2785	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
120	119	eqeq2d 2744	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
121	120	3expa 1119	. . . . . . . 8 ⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
122	121	ralbidva 3176	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
123	122	pm5.32da 580	. . . . . 6 ⊢ (𝑥 ∈ On → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
124	123	rexbiia 3093	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
125	124	abbii 2803	. . . 4 ⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
126	125	unieqi 4922	. . 3 ⊢ ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
127	10, 11, 126	3eqtri 2765	. 2 ⊢ rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
128	9, 127	vtoclg 3557	1 ⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ w3o 1087   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  ifcif 4529  ∪ cuni 4909   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   ↾ cres 5679   “ cima 5680  Rel wrel 5682  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367   Fn wfn 6539  ‘cfv 6544  recscrecs 8370  reccrdg 8409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fo 6550  df-fv 6552  df-ov 7412  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410

This theorem is referenced by:  dfrdg3  34799