Metamath Proof Explorer

Theorem difsnen

Description: All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015)

Ref Expression
Assertion difsnen 
|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( X \ { A } ) ~~ ( X \ { B } ) )

Proof

Step Hyp Ref Expression
1 difexg 
 |-  ( X e. V -> ( X \ { A } ) e. _V )
2 enrefg 
 |-  ( ( X \ { A } ) e. _V -> ( X \ { A } ) ~~ ( X \ { A } ) )
3 1 2 syl 
 |-  ( X e. V -> ( X \ { A } ) ~~ ( X \ { A } ) )
4 3 3ad2ant1 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( X \ { A } ) ~~ ( X \ { A } ) )
5 sneq 
 |-  ( A = B -> { A } = { B } )
6 5 difeq2d 
 |-  ( A = B -> ( X \ { A } ) = ( X \ { B } ) )
7 6 breq2d 
 |-  ( A = B -> ( ( X \ { A } ) ~~ ( X \ { A } ) <-> ( X \ { A } ) ~~ ( X \ { B } ) ) )
8 4 7 syl5ibcom 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( A = B -> ( X \ { A } ) ~~ ( X \ { B } ) ) )
9 8 imp 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A = B ) -> ( X \ { A } ) ~~ ( X \ { B } ) )
10 simpl1 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> X e. V )
11 difexg 
 |-  ( ( X \ { A } ) e. _V -> ( ( X \ { A } ) \ { B } ) e. _V )
12 enrefg 
 |-  ( ( ( X \ { A } ) \ { B } ) e. _V -> ( ( X \ { A } ) \ { B } ) ~~ ( ( X \ { A } ) \ { B } ) )
13 10 1 11 12 4syl 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( X \ { A } ) \ { B } ) ~~ ( ( X \ { A } ) \ { B } ) )
14 dif32 
 |-  ( ( X \ { A } ) \ { B } ) = ( ( X \ { B } ) \ { A } )
15 13 14 breqtrdi 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( X \ { A } ) \ { B } ) ~~ ( ( X \ { B } ) \ { A } ) )
16 simpl3 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> B e. X )
17 simpl2 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> A e. X )
18 en2sn 
 |-  ( ( B e. X /\ A e. X ) -> { B } ~~ { A } )
19 16 17 18 syl2anc 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> { B } ~~ { A } )
20 incom 
 |-  ( ( ( X \ { A } ) \ { B } ) i^i { B } ) = ( { B } i^i ( ( X \ { A } ) \ { B } ) )
21 disjdif 
 |-  ( { B } i^i ( ( X \ { A } ) \ { B } ) ) = (/)
22 20 21 eqtri 
 |-  ( ( ( X \ { A } ) \ { B } ) i^i { B } ) = (/)
23 22 a1i 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { A } ) \ { B } ) i^i { B } ) = (/) )
24 incom 
 |-  ( ( ( X \ { B } ) \ { A } ) i^i { A } ) = ( { A } i^i ( ( X \ { B } ) \ { A } ) )
25 disjdif 
 |-  ( { A } i^i ( ( X \ { B } ) \ { A } ) ) = (/)
26 24 25 eqtri 
 |-  ( ( ( X \ { B } ) \ { A } ) i^i { A } ) = (/)
27 26 a1i 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { B } ) \ { A } ) i^i { A } ) = (/) )
28 unen 
 |-  ( ( ( ( ( X \ { A } ) \ { B } ) ~~ ( ( X \ { B } ) \ { A } ) /\ { B } ~~ { A } ) /\ ( ( ( ( X \ { A } ) \ { B } ) i^i { B } ) = (/) /\ ( ( ( X \ { B } ) \ { A } ) i^i { A } ) = (/) ) ) -> ( ( ( X \ { A } ) \ { B } ) u. { B } ) ~~ ( ( ( X \ { B } ) \ { A } ) u. { A } ) )
29 15 19 23 27 28 syl22anc 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { A } ) \ { B } ) u. { B } ) ~~ ( ( ( X \ { B } ) \ { A } ) u. { A } ) )
30 simpr 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> A =/= B )
31 30 necomd 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> B =/= A )
32 eldifsn 
 |-  ( B e. ( X \ { A } ) <-> ( B e. X /\ B =/= A ) )
33 16 31 32 sylanbrc 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> B e. ( X \ { A } ) )
34 difsnid 
 |-  ( B e. ( X \ { A } ) -> ( ( ( X \ { A } ) \ { B } ) u. { B } ) = ( X \ { A } ) )
35 33 34 syl 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { A } ) \ { B } ) u. { B } ) = ( X \ { A } ) )
36 eldifsn 
 |-  ( A e. ( X \ { B } ) <-> ( A e. X /\ A =/= B ) )
37 17 30 36 sylanbrc 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> A e. ( X \ { B } ) )
38 difsnid 
 |-  ( A e. ( X \ { B } ) -> ( ( ( X \ { B } ) \ { A } ) u. { A } ) = ( X \ { B } ) )
39 37 38 syl 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { B } ) \ { A } ) u. { A } ) = ( X \ { B } ) )
40 29 35 39 3brtr3d 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( X \ { A } ) ~~ ( X \ { B } ) )
41 9 40 pm2.61dane 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( X \ { A } ) ~~ ( X \ { B } ) )