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

Metamath Proof Explorer

Theorem domtri2

Description: Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion domtri2 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 carddom2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )
2 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
3 cardon ⊢ ( card ‘ 𝐵 ) ∈ On
4 ontri1 ⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ) )
5 2 3 4 mp2an ⊢ ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) )
6 cardsdom2 ⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ↔ 𝐵 ≺ 𝐴 ) )
7 6 ancoms ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ↔ 𝐵 ≺ 𝐴 ) )
8 7 notbid ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ↔ ¬ 𝐵 ≺ 𝐴 ) )
9 5 8 bitrid ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ 𝐵 ≺ 𝐴 ) )
10 1 9 bitr3d ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )