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 disjdifr 
 |-  ( ( ( X \ { A } ) \ { B } ) i^i { B } ) = (/)
21 20 a1i 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { A } ) \ { B } ) i^i { B } ) = (/) )
22 disjdifr 
 |-  ( ( ( X \ { B } ) \ { A } ) i^i { A } ) = (/)
23 22 a1i 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { B } ) \ { A } ) i^i { A } ) = (/) )
24 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 } ) )
25 15 19 21 23 24 syl22anc 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { A } ) \ { B } ) u. { B } ) ~~ ( ( ( X \ { B } ) \ { A } ) u. { A } ) )
26 simpr 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> A =/= B )
27 26 necomd 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> B =/= A )
28 eldifsn 
 |-  ( B e. ( X \ { A } ) <-> ( B e. X /\ B =/= A ) )
29 16 27 28 sylanbrc 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> B e. ( X \ { A } ) )
30 difsnid 
 |-  ( B e. ( X \ { A } ) -> ( ( ( X \ { A } ) \ { B } ) u. { B } ) = ( X \ { A } ) )
31 29 30 syl 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { A } ) \ { B } ) u. { B } ) = ( X \ { A } ) )
32 eldifsn 
 |-  ( A e. ( X \ { B } ) <-> ( A e. X /\ A =/= B ) )
33 17 26 32 sylanbrc 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> A e. ( X \ { B } ) )
34 difsnid 
 |-  ( A e. ( X \ { B } ) -> ( ( ( X \ { B } ) \ { A } ) u. { A } ) = ( X \ { B } ) )
35 33 34 syl 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( ( ( X \ { B } ) \ { A } ) u. { A } ) = ( X \ { B } ) )
36 25 31 35 3brtr3d 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ A =/= B ) -> ( X \ { A } ) ~~ ( X \ { B } ) )
37 9 36 pm2.61dane 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( X \ { A } ) ~~ ( X \ { B } ) )