Theorem dfrdg2 36380

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 8405	. . 3 ⊢ (𝑖 = 𝐼 → rec(𝐹, 𝑖) = rec(𝐹, 𝐼))
2		ifeq1 4489	. . . . . . . . 9 ⊢ (𝑖 = 𝐼 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
3	2	eqeq2d 2773	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → ((𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
4	3	ralbidv 3187	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
5	4	anbi2d 642	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
6	5	rexbidv 3188	. . . . 5 ⊢ (𝑖 = 𝐼 → (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
7	6	abbidv 2828	. . . 4 ⊢ (𝑖 = 𝐼 → {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
8	7	unieqd 4883	. . 3 ⊢ (𝑖 = 𝐼 → ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
9	1, 8	eqeq12d 2778	. 2 ⊢ (𝑖 = 𝐼 → (rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} ↔ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}))
10		df-rdg 8403	. . 3 ⊢ rec(𝐹, 𝑖) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))))
11		dfrecs3 8365	. . 3 ⊢ recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))}
12		vex 3457	. . . . . . . . . . . . 13 ⊢ 𝑓 ∈ V
13	12	resex 6026	. . . . . . . . . . . 12 ⊢ (𝑓 ↾ 𝑦) ∈ V
14		eqeq1 2766	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ (𝑓 ↾ 𝑦) = ∅))
15		relres 6002	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑓 ↾ 𝑦)
16		reldm0 5916	. . . . . . . . . . . . . . . 16 ⊢ (Rel (𝑓 ↾ 𝑦) → ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅))
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅)
18	14, 17	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅))
19		dmeq 5891	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → dom 𝑔 = dom (𝑓 ↾ 𝑦))
20		limeq 6373	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑔 = dom (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦)))
21	19, 20	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦)))
22		rneq 5924	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = ran (𝑓 ↾ 𝑦))
23		df-ima 5672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 “ 𝑦) = ran (𝑓 ↾ 𝑦)
24	22, 23	eqtr4di 2815	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = (𝑓 “ 𝑦))
25	24	unieqd 4883	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ ran 𝑔 = ∪ (𝑓 “ 𝑦))
26		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → 𝑔 = (𝑓 ↾ 𝑦))
27	19	unieqd 4883	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ dom 𝑔 = ∪ dom (𝑓 ↾ 𝑦))
28	26, 27	fveq12d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔‘∪ dom 𝑔) = ((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))
29	28	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝐹‘(𝑔‘∪ dom 𝑔)) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))
30	21, 25, 29	ifbieq12d 4514	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))) = if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))))
31	18, 30	ifbieq2d 4512	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))))
32		eqid 2762	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))
33		vex 3457	. . . . . . . . . . . . . 14 ⊢ 𝑖 ∈ V
34		imaexg 7914	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ V → (𝑓 “ 𝑦) ∈ V)
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 “ 𝑦) ∈ V
36	35	uniex 7747	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑓 “ 𝑦) ∈ V
37		fvex 6895	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))) ∈ V
38	36, 37	ifex 4536	. . . . . . . . . . . . . 14 ⊢ if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))) ∈ V
39	33, 38	ifex 4536	. . . . . . . . . . . . 13 ⊢ if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) ∈ V
40	31, 32, 39	fvmpt 6990	. . . . . . . . . . . 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 6009	. . . . . . . . . . . . 13 ⊢ dom (𝑓 ↾ 𝑦) = (𝑦 ∩ dom 𝑓)
43		onelss 6404	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ On → (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥))
44	43	imp 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥)
45	44	3adant2 1149	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥)
46		fndm 6639	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥)
47	46	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom 𝑓 = 𝑥)
48	45, 47	sseqtrrd 3971	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ dom 𝑓)
49		dfss2 3920	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ dom 𝑓 ↔ (𝑦 ∩ dom 𝑓) = 𝑦)
50	48, 49	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ dom 𝑓) = 𝑦)
51	42, 50	eqtrid 2809	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom (𝑓 ↾ 𝑦) = 𝑦)
52		eqeq1 2766	. . . . . . . . . . . . . 14 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (dom (𝑓 ↾ 𝑦) = ∅ ↔ 𝑦 = ∅))
53		limeq 6373	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (Lim dom (𝑓 ↾ 𝑦) ↔ Lim 𝑦))
54		unieq 4881	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → ∪ dom (𝑓 ↾ 𝑦) = ∪ 𝑦)
55	54	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → ((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)) = ((𝑓 ↾ 𝑦)‘∪ 𝑦))
56	55	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))
57	53, 56	ifbieq2d 4512	. . . . . . . . . . . . . 14 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))))
58	52, 57	ifbieq2d 4512	. . . . . . . . . . . . 13 ⊢ (dom (𝑓 ↾ 𝑦) = 𝑦 → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))))
59		onelon 6386	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
60		eloni 6371	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → Ord 𝑦)
61	59, 60	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
62	61	3adant2 1149	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
63		ordzsl 7845	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝑦 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦))
64		iftrue 4491	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = 𝑖)
65		iftrue 4491	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = 𝑖)
66	64, 65	eqtr4d 2800	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
67		vex 3457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
68	67	sucid 6446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑧 ∈ suc 𝑧
69		fvres 6901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ suc 𝑧 → ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧))
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧)
71		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ On → Ord 𝑧)
72		ordunisuc 7832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑧 → ∪ suc 𝑧 = 𝑧)
73	71, 72	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ On → ∪ suc 𝑧 = 𝑧)
74	73	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧) = ((𝑓 ↾ suc 𝑧)‘𝑧))
75	73	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑓‘∪ suc 𝑧) = (𝑓‘𝑧))
76	70, 74, 75	3eqtr4a 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧) = (𝑓‘∪ suc 𝑧))
77	76	fveq2d 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ On → (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
78		nsuceq0 6447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑧 ≠ ∅
79	78	neii 2959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ suc 𝑧 = ∅
80	79	iffalsei 4495	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))
81		nlimsucg 7842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ V → ¬ Lim suc 𝑧)
82		iffalse 4494	. . . . . . . . . . . . . . . . . . . . 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 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))
85	79	iffalsei 4495	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))
86		iffalse 4494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)))
87	67, 81, 86	mp2b 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))
88	85, 87	eqtri 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧))
89	77, 84, 88	3eqtr4g 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ On → if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
90		eqeq1 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
91		limeq 6373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
92		reseq2 5971	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = suc 𝑧 → (𝑓 ↾ 𝑦) = (𝑓 ↾ suc 𝑧))
93		unieq 4881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧)
94	92, 93	fveq12d 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = suc 𝑧 → ((𝑓 ↾ 𝑦)‘∪ 𝑦) = ((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))
95	94	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))
96	91, 95	ifbieq2d 4512	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧))))
97	90, 96	ifbieq2d 4512	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc 𝑧)))))
98	93	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧))
99	98	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
100	91, 99	ifbieq2d 4512	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))
101	90, 100	ifbieq2d 4512	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
102	97, 101	eqeq12d 2778	. . . . . . . . . . . . . . . . . 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 3158	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
105		iftrue 4491	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
106		df-lim 6366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Lim 𝑦 ↔ (Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦))
107	106	simp2bi 1164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Lim 𝑦 → 𝑦 ≠ ∅)
108	107	neneqd 2962	. . . . . . . . . . . . . . . . . . 19 ⊢ (Lim 𝑦 → ¬ 𝑦 = ∅)
109	108	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))))
110		iftrue 4491	. . . . . . . . . . . . . . . . . 18 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
111	105, 109, 110	3eqtr4d 2807	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
112	108	iffalsed 4496	. . . . . . . . . . . . . . . . 17 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
113	111, 112	eqtr4d 2800	. . . . . . . . . . . . . . . 16 ⊢ (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
114	66, 104, 113	3jaoi 1454	. . . . . . . . . . . . . . 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 2819	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) ∧ dom (𝑓 ↾ 𝑦) = 𝑦) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
118	51, 117	mpdan 700	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom (𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
119	41, 118	eqtrid 2809	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))
120	119	eqeq2d 2773	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
121	120	3expa 1136	. . . . . . . 8 ⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
122	121	ralbidva 3185	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
123	122	pm5.32da 590	. . . . . 6 ⊢ (𝑥 ∈ On → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
124	123	rexbiia 3109	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
125	124	abbii 2829	. . . 4 ⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
126	125	unieqi 4882	. . 3 ⊢ ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
127	10, 11, 126	3eqtri 2789	. 2 ⊢ rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
128	9, 127	vtoclg 3520	1 ⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  {cab 2740   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  Vcvv 3453   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282  ifcif 4485  ∪ cuni 4870   ↦ cmpt 5190  dom cdm 5659  ran crn 5660   ↾ cres 5661   “ cima 5662  Rel wrel 5664  Ord word 6360  Oncon0 6361  Lim wlim 6362  suc csuc 6363   Fn wfn 6532  ‘cfv 6537  recscrecs 8363  reccrdg 8402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fo 6543  df-fv 6545  df-ov 7420  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403

This theorem is used by:  dfrdg3  36381