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

Metamath Proof Explorer

Theorem pssdifcom1

Description: Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014)

Ref Expression
Assertion pssdifcom1 ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ 𝐴 ) ⊊ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊊ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 difcom ⊢ ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 )
2 1 a1i ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 ) )
3 ssconb ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐶 ) → ( 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
4 3 ancoms ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
5 4 notbid ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ¬ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ↔ ¬ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
6 2 5 anbi12d ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ) ↔ ( ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 ∧ ¬ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) ) )
7 dfpss3 ⊢ ( ( 𝐶 ∖ 𝐴 ) ⊊ 𝐵 ↔ ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ) )
8 dfpss3 ⊢ ( ( 𝐶 ∖ 𝐵 ) ⊊ 𝐴 ↔ ( ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 ∧ ¬ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
9 6 7 8 3bitr4g ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ 𝐴 ) ⊊ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊊ 𝐴 ) )