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

Metamath Proof Explorer

Theorem disjpss

Description: A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004)

Ref Expression
Assertion disjpss ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐵 ≠ ∅ ) → 𝐴 ⊊ ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssid ⊢ 𝐵 ⊆ 𝐵
2 1 biantru ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵 ) )
3 ssin ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵 ) ↔ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) )
4 2 3 bitri ⊢ ( 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) )
5 sseq2 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ 𝐵 ⊆ ∅ ) )
6 4 5 bitrid ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ ∅ ) )
7 ss0 ⊢ ( 𝐵 ⊆ ∅ → 𝐵 = ∅ )
8 6 7 biimtrdi ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐵 ⊆ 𝐴 → 𝐵 = ∅ ) )
9 8 necon3ad ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐵 ≠ ∅ → ¬ 𝐵 ⊆ 𝐴 ) )
10 9 imp ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐵 ≠ ∅ ) → ¬ 𝐵 ⊆ 𝐴 )
11 nsspssun ⊢ ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐵 ∪ 𝐴 ) )
12 uncom ⊢ ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 )
13 12 psseq2i ⊢ ( 𝐴 ⊊ ( 𝐵 ∪ 𝐴 ) ↔ 𝐴 ⊊ ( 𝐴 ∪ 𝐵 ) )
14 11 13 bitri ⊢ ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∪ 𝐵 ) )
15 10 14 sylib ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐵 ≠ ∅ ) → 𝐴 ⊊ ( 𝐴 ∪ 𝐵 ) )