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

Metamath Proof Explorer

Theorem infdiffi

Description: Removing a finite set from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion infdiffi 
|- ( ( _om ~<_ A /\ B e. Fin ) -> ( A \ B ) ~~ A )

Proof

Step Hyp Ref Expression
1 difeq2 
 |-  ( x = (/) -> ( A \ x ) = ( A \ (/) ) )
2 dif0 
 |-  ( A \ (/) ) = A
3 1 2 eqtrdi 
 |-  ( x = (/) -> ( A \ x ) = A )
4 3 breq1d 
 |-  ( x = (/) -> ( ( A \ x ) ~~ A <-> A ~~ A ) )
5 4 imbi2d 
 |-  ( x = (/) -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> A ~~ A ) ) )
6 difeq2 
 |-  ( x = y -> ( A \ x ) = ( A \ y ) )
7 6 breq1d 
 |-  ( x = y -> ( ( A \ x ) ~~ A <-> ( A \ y ) ~~ A ) )
8 7 imbi2d 
 |-  ( x = y -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> ( A \ y ) ~~ A ) ) )
9 difeq2 
 |-  ( x = ( y u. { z } ) -> ( A \ x ) = ( A \ ( y u. { z } ) ) )
10 difun1 
 |-  ( A \ ( y u. { z } ) ) = ( ( A \ y ) \ { z } )
11 9 10 eqtrdi 
 |-  ( x = ( y u. { z } ) -> ( A \ x ) = ( ( A \ y ) \ { z } ) )
12 11 breq1d 
 |-  ( x = ( y u. { z } ) -> ( ( A \ x ) ~~ A <-> ( ( A \ y ) \ { z } ) ~~ A ) )
13 12 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> ( ( A \ y ) \ { z } ) ~~ A ) ) )
14 difeq2 
 |-  ( x = B -> ( A \ x ) = ( A \ B ) )
15 14 breq1d 
 |-  ( x = B -> ( ( A \ x ) ~~ A <-> ( A \ B ) ~~ A ) )
16 15 imbi2d 
 |-  ( x = B -> ( ( _om ~<_ A -> ( A \ x ) ~~ A ) <-> ( _om ~<_ A -> ( A \ B ) ~~ A ) ) )
17 reldom 
 |-  Rel ~<_
18 17 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
19 enrefg 
 |-  ( A e. _V -> A ~~ A )
20 18 19 syl 
 |-  ( _om ~<_ A -> A ~~ A )
21 domen2 
 |-  ( ( A \ y ) ~~ A -> ( _om ~<_ ( A \ y ) <-> _om ~<_ A ) )
22 21 biimparc 
 |-  ( ( _om ~<_ A /\ ( A \ y ) ~~ A ) -> _om ~<_ ( A \ y ) )
23 infdifsn 
 |-  ( _om ~<_ ( A \ y ) -> ( ( A \ y ) \ { z } ) ~~ ( A \ y ) )
24 22 23 syl 
 |-  ( ( _om ~<_ A /\ ( A \ y ) ~~ A ) -> ( ( A \ y ) \ { z } ) ~~ ( A \ y ) )
25 entr 
 |-  ( ( ( ( A \ y ) \ { z } ) ~~ ( A \ y ) /\ ( A \ y ) ~~ A ) -> ( ( A \ y ) \ { z } ) ~~ A )
26 24 25 sylancom 
 |-  ( ( _om ~<_ A /\ ( A \ y ) ~~ A ) -> ( ( A \ y ) \ { z } ) ~~ A )
27 26 ex 
 |-  ( _om ~<_ A -> ( ( A \ y ) ~~ A -> ( ( A \ y ) \ { z } ) ~~ A ) )
28 27 a2i 
 |-  ( ( _om ~<_ A -> ( A \ y ) ~~ A ) -> ( _om ~<_ A -> ( ( A \ y ) \ { z } ) ~~ A ) )
29 28 a1i 
 |-  ( y e. Fin -> ( ( _om ~<_ A -> ( A \ y ) ~~ A ) -> ( _om ~<_ A -> ( ( A \ y ) \ { z } ) ~~ A ) ) )
30 5 8 13 16 20 29 findcard2 
 |-  ( B e. Fin -> ( _om ~<_ A -> ( A \ B ) ~~ A ) )
31 30 impcom 
 |-  ( ( _om ~<_ A /\ B e. Fin ) -> ( A \ B ) ~~ A )