Metamath Proof Explorer

Theorem disjdifprg

Description: A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion disjdifprg 
|- ( ( A e. V /\ B e. W ) -> Disj_ x e. { ( B \ A ) , A } x )

Proof

Step Hyp Ref Expression
1 disjxsn 
 |-  Disj_ x e. { (/) } x
2 simpr 
 |-  ( ( B e. W /\ B = (/) ) -> B = (/) )
3 eqidd 
 |-  ( ( B e. W /\ B = (/) ) -> (/) = (/) )
4 id 
 |-  ( B e. W -> B e. W )
5 0ex 
 |-  (/) e. _V
6 5 a1i 
 |-  ( B e. W -> (/) e. _V )
7 4 6 preqsnd 
 |-  ( B e. W -> ( { B , (/) } = { (/) } <-> ( B = (/) /\ (/) = (/) ) ) )
8 7 adantr 
 |-  ( ( B e. W /\ B = (/) ) -> ( { B , (/) } = { (/) } <-> ( B = (/) /\ (/) = (/) ) ) )
9 2 3 8 mpbir2and 
 |-  ( ( B e. W /\ B = (/) ) -> { B , (/) } = { (/) } )
10 9 disjeq1d 
 |-  ( ( B e. W /\ B = (/) ) -> ( Disj_ x e. { B , (/) } x <-> Disj_ x e. { (/) } x ) )
11 1 10 mpbiri 
 |-  ( ( B e. W /\ B = (/) ) -> Disj_ x e. { B , (/) } x )
12 in0 
 |-  ( B i^i (/) ) = (/)
13 elex 
 |-  ( B e. W -> B e. _V )
14 13 adantr 
 |-  ( ( B e. W /\ B =/= (/) ) -> B e. _V )
15 5 a1i 
 |-  ( ( B e. W /\ B =/= (/) ) -> (/) e. _V )
16 simpr 
 |-  ( ( B e. W /\ B =/= (/) ) -> B =/= (/) )
17 id 
 |-  ( x = B -> x = B )
18 id 
 |-  ( x = (/) -> x = (/) )
19 17 18 disjprg 
 |-  ( ( B e. _V /\ (/) e. _V /\ B =/= (/) ) -> ( Disj_ x e. { B , (/) } x <-> ( B i^i (/) ) = (/) ) )
20 14 15 16 19 syl3anc 
 |-  ( ( B e. W /\ B =/= (/) ) -> ( Disj_ x e. { B , (/) } x <-> ( B i^i (/) ) = (/) ) )
21 12 20 mpbiri 
 |-  ( ( B e. W /\ B =/= (/) ) -> Disj_ x e. { B , (/) } x )
22 11 21 pm2.61dane 
 |-  ( B e. W -> Disj_ x e. { B , (/) } x )
23 22 ad2antlr 
 |-  ( ( ( A e. V /\ B e. W ) /\ A = (/) ) -> Disj_ x e. { B , (/) } x )
24 difeq2 
 |-  ( A = (/) -> ( B \ A ) = ( B \ (/) ) )
25 dif0 
 |-  ( B \ (/) ) = B
26 24 25 eqtrdi 
 |-  ( A = (/) -> ( B \ A ) = B )
27 id 
 |-  ( A = (/) -> A = (/) )
28 26 27 preq12d 
 |-  ( A = (/) -> { ( B \ A ) , A } = { B , (/) } )
29 28 disjeq1d 
 |-  ( A = (/) -> ( Disj_ x e. { ( B \ A ) , A } x <-> Disj_ x e. { B , (/) } x ) )
30 29 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ A = (/) ) -> ( Disj_ x e. { ( B \ A ) , A } x <-> Disj_ x e. { B , (/) } x ) )
31 23 30 mpbird 
 |-  ( ( ( A e. V /\ B e. W ) /\ A = (/) ) -> Disj_ x e. { ( B \ A ) , A } x )
32 disjdifr 
 |-  ( ( B \ A ) i^i A ) = (/)
33 difexg 
 |-  ( B e. W -> ( B \ A ) e. _V )
34 33 ad2antlr 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A = (/) ) -> ( B \ A ) e. _V )
35 elex 
 |-  ( A e. V -> A e. _V )
36 35 ad2antrr 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A = (/) ) -> A e. _V )
37 ssid 
 |-  ( B \ A ) C_ ( B \ A )
38 ssdifeq0 
 |-  ( A C_ ( B \ A ) <-> A = (/) )
39 38 notbii 
 |-  ( -. A C_ ( B \ A ) <-> -. A = (/) )
40 nssne2 
 |-  ( ( ( B \ A ) C_ ( B \ A ) /\ -. A C_ ( B \ A ) ) -> ( B \ A ) =/= A )
41 39 40 sylan2br 
 |-  ( ( ( B \ A ) C_ ( B \ A ) /\ -. A = (/) ) -> ( B \ A ) =/= A )
42 37 41 mpan 
 |-  ( -. A = (/) -> ( B \ A ) =/= A )
43 42 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A = (/) ) -> ( B \ A ) =/= A )
44 id 
 |-  ( x = ( B \ A ) -> x = ( B \ A ) )
45 id 
 |-  ( x = A -> x = A )
46 44 45 disjprg 
 |-  ( ( ( B \ A ) e. _V /\ A e. _V /\ ( B \ A ) =/= A ) -> ( Disj_ x e. { ( B \ A ) , A } x <-> ( ( B \ A ) i^i A ) = (/) ) )
47 34 36 43 46 syl3anc 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A = (/) ) -> ( Disj_ x e. { ( B \ A ) , A } x <-> ( ( B \ A ) i^i A ) = (/) ) )
48 32 47 mpbiri 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A = (/) ) -> Disj_ x e. { ( B \ A ) , A } x )
49 31 48 pm2.61dan 
 |-  ( ( A e. V /\ B e. W ) -> Disj_ x e. { ( B \ A ) , A } x )