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 
|- ( ( ( A i^i B ) = (/) /\ B =/= (/) ) -> A C. ( A u. B ) )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  B C_ B
2 1 biantru 
 |-  ( B C_ A <-> ( B C_ A /\ B C_ B ) )
3 ssin 
 |-  ( ( B C_ A /\ B C_ B ) <-> B C_ ( A i^i B ) )
4 2 3 bitri 
 |-  ( B C_ A <-> B C_ ( A i^i B ) )
5 sseq2 
 |-  ( ( A i^i B ) = (/) -> ( B C_ ( A i^i B ) <-> B C_ (/) ) )
6 4 5 bitrid 
 |-  ( ( A i^i B ) = (/) -> ( B C_ A <-> B C_ (/) ) )
7 ss0 
 |-  ( B C_ (/) -> B = (/) )
8 6 7 syl6bi 
 |-  ( ( A i^i B ) = (/) -> ( B C_ A -> B = (/) ) )
9 8 necon3ad 
 |-  ( ( A i^i B ) = (/) -> ( B =/= (/) -> -. B C_ A ) )
10 9 imp 
 |-  ( ( ( A i^i B ) = (/) /\ B =/= (/) ) -> -. B C_ A )
11 nsspssun 
 |-  ( -. B C_ A <-> A C. ( B u. A ) )
12 uncom 
 |-  ( B u. A ) = ( A u. B )
13 12 psseq2i 
 |-  ( A C. ( B u. A ) <-> A C. ( A u. B ) )
14 11 13 bitri 
 |-  ( -. B C_ A <-> A C. ( A u. B ) )
15 10 14 sylib 
 |-  ( ( ( A i^i B ) = (/) /\ B =/= (/) ) -> A C. ( A u. B ) )