Metamath Proof Explorer


Theorem tz7.44-1

Description: The value of F at (/) . Part 1 of Theorem 7.44 of TakeutiZaring p. 49. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypotheses tz7.44.1 𝐺 = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ran 𝑥 , ( 𝐻 ‘ ( 𝑥 dom 𝑥 ) ) ) ) )
tz7.44.2 ( 𝑦𝑋 → ( 𝐹𝑦 ) = ( 𝐺 ‘ ( 𝐹𝑦 ) ) )
tz7.44-1.3 𝐴 ∈ V
Assertion tz7.44-1 ( ∅ ∈ 𝑋 → ( 𝐹 ‘ ∅ ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 tz7.44.1 𝐺 = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ran 𝑥 , ( 𝐻 ‘ ( 𝑥 dom 𝑥 ) ) ) ) )
2 tz7.44.2 ( 𝑦𝑋 → ( 𝐹𝑦 ) = ( 𝐺 ‘ ( 𝐹𝑦 ) ) )
3 tz7.44-1.3 𝐴 ∈ V
4 fveq2 ( 𝑦 = ∅ → ( 𝐹𝑦 ) = ( 𝐹 ‘ ∅ ) )
5 reseq2 ( 𝑦 = ∅ → ( 𝐹𝑦 ) = ( 𝐹 ↾ ∅ ) )
6 res0 ( 𝐹 ↾ ∅ ) = ∅
7 5 6 eqtrdi ( 𝑦 = ∅ → ( 𝐹𝑦 ) = ∅ )
8 7 fveq2d ( 𝑦 = ∅ → ( 𝐺 ‘ ( 𝐹𝑦 ) ) = ( 𝐺 ‘ ∅ ) )
9 4 8 eqeq12d ( 𝑦 = ∅ → ( ( 𝐹𝑦 ) = ( 𝐺 ‘ ( 𝐹𝑦 ) ) ↔ ( 𝐹 ‘ ∅ ) = ( 𝐺 ‘ ∅ ) ) )
10 9 2 vtoclga ( ∅ ∈ 𝑋 → ( 𝐹 ‘ ∅ ) = ( 𝐺 ‘ ∅ ) )
11 0ex ∅ ∈ V
12 iftrue ( 𝑥 = ∅ → if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ran 𝑥 , ( 𝐻 ‘ ( 𝑥 dom 𝑥 ) ) ) ) = 𝐴 )
13 12 1 3 fvmpt ( ∅ ∈ V → ( 𝐺 ‘ ∅ ) = 𝐴 )
14 11 13 ax-mp ( 𝐺 ‘ ∅ ) = 𝐴
15 10 14 eqtrdi ( ∅ ∈ 𝑋 → ( 𝐹 ‘ ∅ ) = 𝐴 )