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

Metamath Proof Explorer

Theorem pssdifcom2

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

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

Proof

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