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 ‘ 𝐵 ) ) )