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

Metamath Proof Explorer

Theorem fiprc

Description: The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008)

Ref Expression
Assertion fiprc 
|- Fin e/ _V

Proof

Step Hyp Ref Expression
1 snnex 
 |-  { x | E. y x = { y } } e/ _V
2 snfi 
 |-  { y } e. Fin
3 eleq1 
 |-  ( x = { y } -> ( x e. Fin <-> { y } e. Fin ) )
4 2 3 mpbiri 
 |-  ( x = { y } -> x e. Fin )
5 4 exlimiv 
 |-  ( E. y x = { y } -> x e. Fin )
6 5 abssi 
 |-  { x | E. y x = { y } } C_ Fin
7 ssexg 
 |-  ( ( { x | E. y x = { y } } C_ Fin /\ Fin e. _V ) -> { x | E. y x = { y } } e. _V )
8 6 7 mpan 
 |-  ( Fin e. _V -> { x | E. y x = { y } } e. _V )
9 8 con3i 
 |-  ( -. { x | E. y x = { y } } e. _V -> -. Fin e. _V )
10 df-nel 
 |-  ( { x | E. y x = { y } } e/ _V <-> -. { x | E. y x = { y } } e. _V )
11 df-nel 
 |-  ( Fin e/ _V <-> -. Fin e. _V )
12 9 10 11 3imtr4i 
 |-  ( { x | E. y x = { y } } e/ _V -> Fin e/ _V )
13 1 12 ax-mp 
 |-  Fin e/ _V