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

Metamath Proof Explorer

Theorem infn0ALT

Description: Shorter proof of infn0 using ax-un . (Contributed by NM, 23-Oct-2004) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	infn0ALT	⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		peano1	⊢ ∅ ∈ ω
2		infsdomnn	⊢ ( ( ω ≼ 𝐴 ∧ ∅ ∈ ω ) → ∅ ≺ 𝐴 )
3	1 2	mpan2	⊢ ( ω ≼ 𝐴 → ∅ ≺ 𝐴 )
4		reldom	⊢ Rel ≼
5	4	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
6		0sdomg	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
7	5 6	syl	⊢ ( ω ≼ 𝐴 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
8	3 7	mpbid	⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ )