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	syl6bi	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐵 ⊆ 𝐴 → 𝐵 = ∅ ) )
9	8	necon3ad	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐵 ≠ ∅ → ¬ 𝐵 ⊆ 𝐴 ) )
10	9	imp	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐵 ≠ ∅ ) → ¬ 𝐵 ⊆ 𝐴 )
11		nsspssun	⊢ ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐵 ∪ 𝐴 ) )
12		uncom	⊢ ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 )
13	12	psseq2i	⊢ ( 𝐴 ⊊ ( 𝐵 ∪ 𝐴 ) ↔ 𝐴 ⊊ ( 𝐴 ∪ 𝐵 ) )
14	11 13	bitri	⊢ ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∪ 𝐵 ) )
15	10 14	sylib	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐵 ≠ ∅ ) → 𝐴 ⊊ ( 𝐴 ∪ 𝐵 ) )