Metamath Proof Explorer

Theorem dfrdg3

Description: Generalization of dfrdg2 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfrdg3 ⊢ rec ⁡ F I = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y

Proof

Step Hyp Ref Expression
1 dfrdg2 ⊢ I ∈ V → rec ⁡ F I = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
2 iftrue ⊢ I ∈ V → if I ∈ V I ∅ = I
3 2 ifeq1d ⊢ I ∈ V → if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
4 3 eqeq2d ⊢ I ∈ V → f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ f ⁡ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
5 4 ralbidv ⊢ I ∈ V → ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∀ y ∈ x f ⁡ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
6 5 anbi2d ⊢ I ∈ V → f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
7 6 rexbidv ⊢ I ∈ V → ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
8 7 abbidv ⊢ I ∈ V → f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
9 8 unieqd ⊢ I ∈ V → ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ I if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
10 1 9 eqtr4d ⊢ I ∈ V → rec ⁡ F I = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
11 0ex ⊢ ∅ ∈ V
12 dfrdg2 ⊢ ∅ ∈ V → rec ⁡ F ∅ = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
13 11 12 ax-mp ⊢ rec ⁡ F ∅ = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
14 rdgprc ⊢ ¬ I ∈ V → rec ⁡ F I = rec ⁡ F ∅
15 iffalse ⊢ ¬ I ∈ V → if I ∈ V I ∅ = ∅
16 15 ifeq1d ⊢ ¬ I ∈ V → if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
17 16 eqeq2d ⊢ ¬ I ∈ V → f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
18 17 ralbidv ⊢ ¬ I ∈ V → ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∀ y ∈ x f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
19 18 anbi2d ⊢ ¬ I ∈ V → f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
20 19 rexbidv ⊢ ¬ I ∈ V → ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
21 20 abbidv ⊢ ¬ I ∈ V → f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
22 21 unieqd ⊢ ¬ I ∈ V → ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
23 13 14 22 3eqtr4a ⊢ ¬ I ∈ V → rec ⁡ F I = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
24 10 23 pm2.61i ⊢ rec ⁡ F I = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if I ∈ V I ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y