This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )

Proof

Step Hyp Ref Expression
1 disjxsn ⊢ Disj 𝑥 ∈ { ∅ } 𝑥
2 simpr ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
3 eqidd ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → ∅ = ∅ )
4 id ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑊 )
5 0ex ⊢ ∅ ∈ V
6 5 a1i ⊢ ( 𝐵 ∈ 𝑊 → ∅ ∈ V )
7 4 6 preqsnd ⊢ ( 𝐵 ∈ 𝑊 → ( { 𝐵 , ∅ } = { ∅ } ↔ ( 𝐵 = ∅ ∧ ∅ = ∅ ) ) )
8 7 adantr ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → ( { 𝐵 , ∅ } = { ∅ } ↔ ( 𝐵 = ∅ ∧ ∅ = ∅ ) ) )
9 2 3 8 mpbir2and ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → { 𝐵 , ∅ } = { ∅ } )
10 9 disjeq1d ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → ( Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ↔ Disj 𝑥 ∈ { ∅ } 𝑥 ) )
11 1 10 mpbiri ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 = ∅ ) → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
12 in0 ⊢ ( 𝐵 ∩ ∅ ) = ∅
13 elex ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
14 13 adantr ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐵 ∈ V )
15 5 a1i ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → ∅ ∈ V )
16 simpr ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 𝐵 ≠ ∅ )
17 id ⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
18 id ⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
19 17 18 disjprg ⊢ ( ( 𝐵 ∈ V ∧ ∅ ∈ V ∧ 𝐵 ≠ ∅ ) → ( Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ↔ ( 𝐵 ∩ ∅ ) = ∅ ) )
20 14 15 16 19 syl3anc ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → ( Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ↔ ( 𝐵 ∩ ∅ ) = ∅ ) )
21 12 20 mpbiri ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
22 11 21 pm2.61dane ⊢ ( 𝐵 ∈ 𝑊 → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
23 22 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = ∅ ) → Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 )
24 difeq2 ⊢ ( 𝐴 = ∅ → ( 𝐵 ∖ 𝐴 ) = ( 𝐵 ∖ ∅ ) )
25 dif0 ⊢ ( 𝐵 ∖ ∅ ) = 𝐵
26 24 25 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝐵 ∖ 𝐴 ) = 𝐵 )
27 id ⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
28 26 27 preq12d ⊢ ( 𝐴 = ∅ → { ( 𝐵 ∖ 𝐴 ) , 𝐴 } = { 𝐵 , ∅ } )
29 28 disjeq1d ⊢ ( 𝐴 = ∅ → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ) )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = ∅ ) → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ Disj 𝑥 ∈ { 𝐵 , ∅ } 𝑥 ) )
31 23 30 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = ∅ ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )
32 disjdifr ⊢ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅
33 difexg ⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∖ 𝐴 ) ∈ V )
34 33 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → ( 𝐵 ∖ 𝐴 ) ∈ V )
35 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
36 35 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → 𝐴 ∈ V )
37 ssid ⊢ ( 𝐵 ∖ 𝐴 ) ⊆ ( 𝐵 ∖ 𝐴 )
38 ssdifeq0 ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ 𝐴 = ∅ )
39 38 notbii ⊢ ( ¬ 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ ¬ 𝐴 = ∅ )
40 nssne2 ⊢ ( ( ( 𝐵 ∖ 𝐴 ) ⊆ ( 𝐵 ∖ 𝐴 ) ∧ ¬ 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
41 39 40 sylan2br ⊢ ( ( ( 𝐵 ∖ 𝐴 ) ⊆ ( 𝐵 ∖ 𝐴 ) ∧ ¬ 𝐴 = ∅ ) → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
42 37 41 mpan ⊢ ( ¬ 𝐴 = ∅ → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
43 42 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 )
44 id ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐴 ) → 𝑥 = ( 𝐵 ∖ 𝐴 ) )
45 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
46 44 45 disjprg ⊢ ( ( ( 𝐵 ∖ 𝐴 ) ∈ V ∧ 𝐴 ∈ V ∧ ( 𝐵 ∖ 𝐴 ) ≠ 𝐴 ) → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅ ) )
47 34 36 43 46 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → ( Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 ↔ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅ ) )
48 32 47 mpbiri ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 = ∅ ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )
49 31 48 pm2.61dan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Disj 𝑥 ∈ { ( 𝐵 ∖ 𝐴 ) , 𝐴 } 𝑥 )