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

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	⊢ ( ∅ ∈ 𝑋 → ( 𝐹 ‘ ∅ ) = 𝐴 )