Metamath Proof Explorer


Theorem harinf

Description: The Hartogs number of an infinite set is at least _om .MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015)

Ref Expression
Assertion harinf S V ¬ S Fin ω har S

Proof

Step Hyp Ref Expression
1 nnon x ω x On
2 1 adantl S V ¬ S Fin x ω x On
3 simplr S V ¬ S Fin x ω ¬ S Fin
4 nnfi x ω x Fin
5 4 adantl S V ¬ S Fin x ω x Fin
6 sdomdom S x S x
7 domfi x Fin S x S Fin
8 7 ex x Fin S x S Fin
9 5 6 8 syl2im S V ¬ S Fin x ω S x S Fin
10 3 9 mtod S V ¬ S Fin x ω ¬ S x
11 simpll S V ¬ S Fin x ω S V
12 fidomtri x Fin S V x S ¬ S x
13 5 11 12 syl2anc S V ¬ S Fin x ω x S ¬ S x
14 10 13 mpbird S V ¬ S Fin x ω x S
15 elharval x har S x On x S
16 2 14 15 sylanbrc S V ¬ S Fin x ω x har S
17 16 ex S V ¬ S Fin x ω x har S
18 17 ssrdv S V ¬ S Fin ω har S