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 ‘ 𝐵 ) ↔ 𝐴 ≺ 𝐵 ) )