This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) }

Proof

Step Hyp Ref Expression
1 dfrdg2 ⊢ ( 𝐼 ∈ V → rec ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
2 iftrue ⊢ ( 𝐼 ∈ V → if ( 𝐼 ∈ V , 𝐼 , ∅ ) = 𝐼 )
3 2 ifeq1d ⊢ ( 𝐼 ∈ V → if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
4 3 eqeq2d ⊢ ( 𝐼 ∈ V → ( ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
5 4 ralbidv ⊢ ( 𝐼 ∈ V → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
6 5 anbi2d ⊢ ( 𝐼 ∈ V → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
7 6 rexbidv ⊢ ( 𝐼 ∈ V → ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
8 7 abbidv ⊢ ( 𝐼 ∈ V → { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
9 8 unieqd ⊢ ( 𝐼 ∈ V → ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
10 1 9 eqtr4d ⊢ ( 𝐼 ∈ V → rec ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
11 0ex ⊢ ∅ ∈ V
12 dfrdg2 ⊢ ( ∅ ∈ V → rec ( 𝐹 , ∅ ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
13 11 12 ax-mp ⊢ rec ( 𝐹 , ∅ ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) }
14 rdgprc ⊢ ( ¬ 𝐼 ∈ V → rec ( 𝐹 , 𝐼 ) = rec ( 𝐹 , ∅ ) )
15 iffalse ⊢ ( ¬ 𝐼 ∈ V → if ( 𝐼 ∈ V , 𝐼 , ∅ ) = ∅ )
16 15 ifeq1d ⊢ ( ¬ 𝐼 ∈ V → if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
17 16 eqeq2d ⊢ ( ¬ 𝐼 ∈ V → ( ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
18 17 ralbidv ⊢ ( ¬ 𝐼 ∈ V → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
19 18 anbi2d ⊢ ( ¬ 𝐼 ∈ V → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
20 19 rexbidv ⊢ ( ¬ 𝐼 ∈ V → ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
21 20 abbidv ⊢ ( ¬ 𝐼 ∈ V → { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
22 21 unieqd ⊢ ( ¬ 𝐼 ∈ V → ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , ∅ , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
23 13 14 22 3eqtr4a ⊢ ( ¬ 𝐼 ∈ V → rec ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
24 10 23 pm2.61i ⊢ rec ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐼 ∈ V , 𝐼 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) }