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 ) → ( 𝐴𝐵𝐴 = 𝐵 ) )