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∈V∧B∈W→Disjx∈B∖AAx

Proof

Step Hyp Ref Expression
1 disjxsn ⊢Disjx∈∅x
2 simpr ⊢B∈W∧B=∅→B=∅
3 eqidd ⊢B∈W∧B=∅→∅=∅
4 id ⊢B∈W→B∈W
5 0ex ⊢∅∈V
6 5 a1i ⊢B∈W→∅∈V
7 4 6 preqsnd ⊢B∈W→B∅=∅↔B=∅∧∅=∅
8 7 adantr ⊢B∈W∧B=∅→B∅=∅↔B=∅∧∅=∅
9 2 3 8 mpbir2and ⊢B∈W∧B=∅→B∅=∅
10 9 disjeq1d ⊢B∈W∧B=∅→Disjx∈B∅x↔Disjx∈∅x
11 1 10 mpbiri ⊢B∈W∧B=∅→Disjx∈B∅x
12 in0 ⊢B∩∅=∅
13 elex ⊢B∈W→B∈V
14 13 adantr ⊢B∈W∧B≠∅→B∈V
15 5 a1i ⊢B∈W∧B≠∅→∅∈V
16 simpr ⊢B∈W∧B≠∅→B≠∅
17 id ⊢x=B→x=B
18 id ⊢x=∅→x=∅
19 17 18 disjprg ⊢B∈V∧∅∈V∧B≠∅→Disjx∈B∅x↔B∩∅=∅
20 14 15 16 19 syl3anc ⊢B∈W∧B≠∅→Disjx∈B∅x↔B∩∅=∅
21 12 20 mpbiri ⊢B∈W∧B≠∅→Disjx∈B∅x
22 11 21 pm2.61dane ⊢B∈W→Disjx∈B∅x
23 22 ad2antlr ⊢A∈V∧B∈W∧A=∅→Disjx∈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∖AA=B∅
29 28 disjeq1d ⊢A=∅→Disjx∈B∖AAx↔Disjx∈B∅x
30 29 adantl ⊢A∈V∧B∈W∧A=∅→Disjx∈B∖AAx↔Disjx∈B∅x
31 23 30 mpbird ⊢A∈V∧B∈W∧A=∅→Disjx∈B∖AAx
32 disjdifr ⊢B∖A∩A=∅
33 difexg ⊢B∈W→B∖A∈V
34 33 ad2antlr ⊢A∈V∧B∈W∧¬A=∅→B∖A∈V
35 elex ⊢A∈V→A∈V
36 35 ad2antrr ⊢A∈V∧B∈W∧¬A=∅→A∈V
37 ssid ⊢B∖A⊆B∖A
38 ssdifeq0 ⊢A⊆B∖A↔A=∅
39 38 notbii ⊢¬A⊆B∖A↔¬A=∅
40 nssne2 ⊢B∖A⊆B∖A∧¬A⊆B∖A→B∖A≠A
41 39 40 sylan2br ⊢B∖A⊆B∖A∧¬A=∅→B∖A≠A
42 37 41 mpan ⊢¬A=∅→B∖A≠A
43 42 adantl ⊢A∈V∧B∈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∈V∧A∈V∧B∖A≠A→Disjx∈B∖AAx↔B∖A∩A=∅
47 34 36 43 46 syl3anc ⊢A∈V∧B∈W∧¬A=∅→Disjx∈B∖AAx↔B∖A∩A=∅
48 32 47 mpbiri ⊢A∈V∧B∈W∧¬A=∅→Disjx∈B∖AAx
49 31 48 pm2.61dan ⊢A∈V∧B∈W→Disjx∈B∖AAx