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 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )

Proof

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