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

Metamath Proof Explorer

Theorem tz9.12lem2

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003)

		Ref	Expression
	Hypotheses	tz9.12lem.1	⊢ 𝐴 ∈ V
		tz9.12lem.2	⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅₁ ‘ 𝑣 ) } )
	Assertion	tz9.12lem2	⊢ suc ∪ ( 𝐹 “ 𝐴 ) ∈ On

Proof

Step	Hyp	Ref	Expression
1		tz9.12lem.1	⊢ 𝐴 ∈ V
2		tz9.12lem.2	⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅₁ ‘ 𝑣 ) } )
3	1 2	tz9.12lem1	⊢ ( 𝐹 “ 𝐴 ) ⊆ On
4	2	funmpt2	⊢ Fun 𝐹
5	1	funimaex	⊢ ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ∈ V )
6	4 5	ax-mp	⊢ ( 𝐹 “ 𝐴 ) ∈ V
7	6	ssonunii	⊢ ( ( 𝐹 “ 𝐴 ) ⊆ On → ∪ ( 𝐹 “ 𝐴 ) ∈ On )
8	3 7	ax-mp	⊢ ∪ ( 𝐹 “ 𝐴 ) ∈ On
9	8	onsuci	⊢ suc ∪ ( 𝐹 “ 𝐴 ) ∈ On