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 𝑦 , ( 𝑓𝑦 ) , ( 𝐹 ‘ ( 𝑓 𝑦 ) ) ) ) ) }