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 ω A A

Proof

Step Hyp Ref Expression
1 peano1 ω
2 infsdomnn ω A ω A
3 1 2 mpan2 ω A A
4 reldom Rel
5 4 brrelex2i ω A A V
6 0sdomg A V A A
7 5 6 syl ω A A A
8 3 7 mpbid ω A A