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

Metamath Proof Explorer

Theorem cardsdom2

Description: A numerable set is strictly dominated by another iff their cardinalities are strictly ordered. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion cardsdom2 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ 𝐴 ≺ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 carddom2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )
2 carden2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
3 2 necon3abid ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ≠ ( card ‘ 𝐵 ) ↔ ¬ 𝐴 ≈ 𝐵 ) )
4 1 3 anbi12d ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ( card ‘ 𝐵 ) ) ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) ) )
5 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
6 cardon ⊢ ( card ‘ 𝐵 ) ∈ On
7 onelpss ⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ( card ‘ 𝐵 ) ) ) )
8 5 6 7 mp2an ⊢ ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ( card ‘ 𝐵 ) ) )
9 brsdom ⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) )
10 4 8 9 3bitr4g ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ↔ 𝐴 ≺ 𝐵 ) )