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

Metamath Proof Explorer

Theorem atsseq

Description: Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atsseq ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 atne0 ⊢ ( 𝐴 ∈ HAtoms → 𝐴 ≠ 0ℋ )
2 1 ad2antrr ⊢ ( ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ≠ 0ℋ )
3 atelch ⊢ ( 𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ )
4 atss ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) )
5 3 4 sylan ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) )
6 5 imp ⊢ ( ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) )
7 6 ord ⊢ ( ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) ∧ 𝐴 ⊆ 𝐵 ) → ( ¬ 𝐴 = 𝐵 → 𝐴 = 0ℋ ) )
8 7 necon1ad ⊢ ( ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ≠ 0ℋ → 𝐴 = 𝐵 ) )
9 2 8 mpd ⊢ ( ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 = 𝐵 )
10 9 ex ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⊆ 𝐵 → 𝐴 = 𝐵 ) )
11 eqimss ⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )
12 10 11 impbid1 ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 = 𝐵 ) )