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

Metamath Proof Explorer

Theorem unir1

Description: The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of Mendelson p. 281. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 8-Jun-2013)

		Ref	Expression
	Assertion	unir1	⊢ ∪ ( 𝑅₁ “ On ) = V

Proof

Step	Hyp	Ref	Expression
1		setind	⊢ ( ∀ 𝑥 ( 𝑥 ⊆ ∪ ( 𝑅₁ “ On ) → 𝑥 ∈ ∪ ( 𝑅₁ “ On ) ) → ∪ ( 𝑅₁ “ On ) = V )
2		vex	⊢ 𝑥 ∈ V
3	2	r1elss	⊢ ( 𝑥 ∈ ∪ ( 𝑅₁ “ On ) ↔ 𝑥 ⊆ ∪ ( 𝑅₁ “ On ) )
4	3	biimpri	⊢ ( 𝑥 ⊆ ∪ ( 𝑅₁ “ On ) → 𝑥 ∈ ∪ ( 𝑅₁ “ On ) )
5	1 4	mpg	⊢ ∪ ( 𝑅₁ “ On ) = V