Metamath Proof Explorer

Theorem carddom2

Description: Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom , which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion carddom2 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 carddomi2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) → 𝐴 ≼ 𝐵 ) )
2 brdom2 ⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
3 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
4 3 onelssi ⊢ ( ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) → ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) )
5 carddomi2 ⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) → 𝐵 ≼ 𝐴 ) )
6 5 ancoms ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) → 𝐵 ≼ 𝐴 ) )
7 domnsym ⊢ ( 𝐵 ≼ 𝐴 → ¬ 𝐴 ≺ 𝐵 )
8 4 6 7 syl56 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) → ¬ 𝐴 ≺ 𝐵 ) )
9 8 con2d ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≺ 𝐵 → ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ) )
10 cardon ⊢ ( card ‘ 𝐵 ) ∈ On
11 ontri1 ⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ) )
12 3 10 11 mp2an ⊢ ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) )
13 9 12 imbitrrdi ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≺ 𝐵 → ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ) )
14 carden2b ⊢ ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )
15 eqimss ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) )
16 14 15 syl ⊢ ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) )
17 16 a1i ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ) )
18 13 17 jaod ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) → ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ) )
19 2 18 biimtrid ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 → ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ) )
20 1 19 impbid ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )