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

Metamath Proof Explorer

Theorem chrelat2

Description: A consequence of relative atomicity. (Contributed by NM, 1-Jul-2004) (New usage is discouraged.)

Ref Expression
Assertion chrelat2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ¬ A ⊆ B ↔ ∃ x ∈ HAtoms x ⊆ A ∧ ¬ x ⊆ B

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ A = if A ∈ C ℋ A ℋ → A ⊆ B ↔ if A ∈ C ℋ A ℋ ⊆ B
2 1 notbid ⊢ A = if A ∈ C ℋ A ℋ → ¬ A ⊆ B ↔ ¬ if A ∈ C ℋ A ℋ ⊆ B
3 sseq2 ⊢ A = if A ∈ C ℋ A ℋ → x ⊆ A ↔ x ⊆ if A ∈ C ℋ A ℋ
4 3 anbi1d ⊢ A = if A ∈ C ℋ A ℋ → x ⊆ A ∧ ¬ x ⊆ B ↔ x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ B
5 4 rexbidv ⊢ A = if A ∈ C ℋ A ℋ → ∃ x ∈ HAtoms x ⊆ A ∧ ¬ x ⊆ B ↔ ∃ x ∈ HAtoms x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ B
6 2 5 bibi12d ⊢ A = if A ∈ C ℋ A ℋ → ¬ A ⊆ B ↔ ∃ x ∈ HAtoms x ⊆ A ∧ ¬ x ⊆ B ↔ ¬ if A ∈ C ℋ A ℋ ⊆ B ↔ ∃ x ∈ HAtoms x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ B
7 sseq2 ⊢ B = if B ∈ C ℋ B ℋ → if A ∈ C ℋ A ℋ ⊆ B ↔ if A ∈ C ℋ A ℋ ⊆ if B ∈ C ℋ B ℋ
8 7 notbid ⊢ B = if B ∈ C ℋ B ℋ → ¬ if A ∈ C ℋ A ℋ ⊆ B ↔ ¬ if A ∈ C ℋ A ℋ ⊆ if B ∈ C ℋ B ℋ
9 sseq2 ⊢ B = if B ∈ C ℋ B ℋ → x ⊆ B ↔ x ⊆ if B ∈ C ℋ B ℋ
10 9 notbid ⊢ B = if B ∈ C ℋ B ℋ → ¬ x ⊆ B ↔ ¬ x ⊆ if B ∈ C ℋ B ℋ
11 10 anbi2d ⊢ B = if B ∈ C ℋ B ℋ → x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ B ↔ x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ if B ∈ C ℋ B ℋ
12 11 rexbidv ⊢ B = if B ∈ C ℋ B ℋ → ∃ x ∈ HAtoms x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ B ↔ ∃ x ∈ HAtoms x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ if B ∈ C ℋ B ℋ
13 8 12 bibi12d ⊢ B = if B ∈ C ℋ B ℋ → ¬ if A ∈ C ℋ A ℋ ⊆ B ↔ ∃ x ∈ HAtoms x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ B ↔ ¬ if A ∈ C ℋ A ℋ ⊆ if B ∈ C ℋ B ℋ ↔ ∃ x ∈ HAtoms x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ if B ∈ C ℋ B ℋ
14 ifchhv ⊢ if A ∈ C ℋ A ℋ ∈ C ℋ
15 ifchhv ⊢ if B ∈ C ℋ B ℋ ∈ C ℋ
16 14 15 chrelat2i ⊢ ¬ if A ∈ C ℋ A ℋ ⊆ if B ∈ C ℋ B ℋ ↔ ∃ x ∈ HAtoms x ⊆ if A ∈ C ℋ A ℋ ∧ ¬ x ⊆ if B ∈ C ℋ B ℋ
17 6 13 16 dedth2h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ¬ A ⊆ B ↔ ∃ x ∈ HAtoms x ⊆ A ∧ ¬ x ⊆ B