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 syl5bb ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ 𝐵𝐴 ) )
10 1 9 bitr3d ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴𝐵 ↔ ¬ 𝐵𝐴 ) )