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