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

Metamath Proof Explorer

Theorem cardsdomel

Description: A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 15-Jan-2013) (Revised by Mario Carneiro, 4-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 cardid2 ⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
2 1 ensymd ⊢ ( 𝐵 ∈ dom card → 𝐵 ≈ ( card ‘ 𝐵 ) )
3 sdomentr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≈ ( card ‘ 𝐵 ) ) → 𝐴 ≺ ( card ‘ 𝐵 ) )
4 2 3 sylan2 ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ∈ dom card ) → 𝐴 ≺ ( card ‘ 𝐵 ) )
5 ssdomg ⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝐵 ) ⊆ 𝐴 → ( card ‘ 𝐵 ) ≼ 𝐴 ) )
6 cardon ⊢ ( card ‘ 𝐵 ) ∈ On
7 domtriord ⊢ ( ( ( card ‘ 𝐵 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( card ‘ 𝐵 ) ≼ 𝐴 ↔ ¬ 𝐴 ≺ ( card ‘ 𝐵 ) ) )
8 6 7 mpan ⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝐵 ) ≼ 𝐴 ↔ ¬ 𝐴 ≺ ( card ‘ 𝐵 ) ) )
9 5 8 sylibd ⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝐵 ) ⊆ 𝐴 → ¬ 𝐴 ≺ ( card ‘ 𝐵 ) ) )
10 9 con2d ⊢ ( 𝐴 ∈ On → ( 𝐴 ≺ ( card ‘ 𝐵 ) → ¬ ( card ‘ 𝐵 ) ⊆ 𝐴 ) )
11 ontri1 ⊢ ( ( ( card ‘ 𝐵 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( card ‘ 𝐵 ) ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ( card ‘ 𝐵 ) ) )
12 6 11 mpan ⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝐵 ) ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ( card ‘ 𝐵 ) ) )
13 12 con2bid ⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ⊆ 𝐴 ) )
14 10 13 sylibrd ⊢ ( 𝐴 ∈ On → ( 𝐴 ≺ ( card ‘ 𝐵 ) → 𝐴 ∈ ( card ‘ 𝐵 ) ) )
15 4 14 syl5 ⊢ ( 𝐴 ∈ On → ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ∈ dom card ) → 𝐴 ∈ ( card ‘ 𝐵 ) ) )
16 15 expcomd ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ dom card → ( 𝐴 ≺ 𝐵 → 𝐴 ∈ ( card ‘ 𝐵 ) ) ) )
17 16 imp ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≺ 𝐵 → 𝐴 ∈ ( card ‘ 𝐵 ) ) )
18 cardsdomelir ⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐴 ≺ 𝐵 )
19 17 18 impbid1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≺ 𝐵 ↔ 𝐴 ∈ ( card ‘ 𝐵 ) ) )