Step |
Hyp |
Ref |
Expression |
1 |
|
cardon |
⊢ ( card ‘ 𝐴 ) ∈ On |
2 |
|
eleq1 |
⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) ) |
3 |
1 2
|
mpbii |
⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ On ) |
4 |
|
cardonle |
⊢ ( 𝐴 ∈ On → ( card ‘ 𝐴 ) ⊆ 𝐴 ) |
5 |
|
eqss |
⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( ( card ‘ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( card ‘ 𝐴 ) ) ) |
6 |
5
|
baibr |
⊢ ( ( card ‘ 𝐴 ) ⊆ 𝐴 → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝐴 ) = 𝐴 ) ) |
7 |
4 6
|
syl |
⊢ ( 𝐴 ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝐴 ) = 𝐴 ) ) |
8 |
|
dfss3 |
⊢ ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( card ‘ 𝐴 ) ) |
9 |
|
onelon |
⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On ) |
10 |
|
onenon |
⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card ) |
11 |
10
|
adantr |
⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ dom card ) |
12 |
|
cardsdomel |
⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ∈ dom card ) → ( 𝑥 ≺ 𝐴 ↔ 𝑥 ∈ ( card ‘ 𝐴 ) ) ) |
13 |
9 11 12
|
syl2anc |
⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≺ 𝐴 ↔ 𝑥 ∈ ( card ‘ 𝐴 ) ) ) |
14 |
13
|
ralbidva |
⊢ ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( card ‘ 𝐴 ) ) ) |
15 |
8 14
|
bitr4id |
⊢ ( 𝐴 ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ) ) |
16 |
7 15
|
bitr3d |
⊢ ( 𝐴 ∈ On → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ) ) |
17 |
3 16
|
biadanii |
⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ) ) |