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 ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )