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 → Disj x ∈ B ∖ A A x

Proof

Step Hyp Ref Expression
1 disjxsn ⊢ Disj x ∈ ∅ 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 = ∅ → Disj x ∈ B ∅ x ↔ Disj x ∈ ∅ x
11 1 10 mpbiri ⊢ B ∈ W ∧ B = ∅ → Disj x ∈ 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 ≠ ∅ → Disj x ∈ B ∅ x ↔ B ∩ ∅ = ∅
20 14 15 16 19 syl3anc ⊢ B ∈ W ∧ B ≠ ∅ → Disj x ∈ B ∅ x ↔ B ∩ ∅ = ∅
21 12 20 mpbiri ⊢ B ∈ W ∧ B ≠ ∅ → Disj x ∈ B ∅ x
22 11 21 pm2.61dane ⊢ B ∈ W → Disj x ∈ B ∅ x
23 22 ad2antlr ⊢ A ∈ V ∧ B ∈ W ∧ A = ∅ → Disj x ∈ 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 ∈ B ∖ A A x ↔ Disj x ∈ B ∅ x
30 29 adantl ⊢ A ∈ V ∧ B ∈ W ∧ A = ∅ → Disj x ∈ B ∖ A A x ↔ Disj x ∈ B ∅ x
31 23 30 mpbird ⊢ A ∈ V ∧ B ∈ W ∧ A = ∅ → Disj x ∈ B ∖ A A x
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 → Disj x ∈ B ∖ A A x ↔ B ∖ A ∩ A = ∅
47 34 36 43 46 syl3anc ⊢ A ∈ V ∧ B ∈ W ∧ ¬ A = ∅ → Disj x ∈ B ∖ A A x ↔ B ∖ A ∩ A = ∅
48 32 47 mpbiri ⊢ A ∈ V ∧ B ∈ W ∧ ¬ A = ∅ → Disj x ∈ B ∖ A A x
49 31 48 pm2.61dan ⊢ A ∈ V ∧ B ∈ W → Disj x ∈ B ∖ A A x