Metamath Proof Explorer

Theorem fin4i

Description: Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015)

Ref Expression
Assertion fin4i 
|- ( ( X C. A /\ X ~~ A ) -> -. A e. Fin4 )

Proof

Step Hyp Ref Expression
1 isfin4 
 |-  ( A e. Fin4 -> ( A e. Fin4 <-> -. E. x ( x C. A /\ x ~~ A ) ) )
2 1 ibi 
 |-  ( A e. Fin4 -> -. E. x ( x C. A /\ x ~~ A ) )
3 relen 
 |-  Rel ~~
4 3 brrelex1i 
 |-  ( X ~~ A -> X e. _V )
5 4 adantl 
 |-  ( ( X C. A /\ X ~~ A ) -> X e. _V )
6 psseq1 
 |-  ( x = X -> ( x C. A <-> X C. A ) )
7 breq1 
 |-  ( x = X -> ( x ~~ A <-> X ~~ A ) )
8 6 7 anbi12d 
 |-  ( x = X -> ( ( x C. A /\ x ~~ A ) <-> ( X C. A /\ X ~~ A ) ) )
9 8 spcegv 
 |-  ( X e. _V -> ( ( X C. A /\ X ~~ A ) -> E. x ( x C. A /\ x ~~ A ) ) )
10 5 9 mpcom 
 |-  ( ( X C. A /\ X ~~ A ) -> E. x ( x C. A /\ x ~~ A ) )
11 2 10 nsyl3 
 |-  ( ( X C. A /\ X ~~ A ) -> -. A e. Fin4 )