Step |
Hyp |
Ref |
Expression |
1 |
|
cfon |
⊢ ( cf ‘ 𝐴 ) ∈ On |
2 |
|
eleq1 |
⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → ( ( cf ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) ) |
3 |
1 2
|
mpbii |
⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ On ) |
4 |
3
|
3ad2ant2 |
⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) → 𝐴 ∈ On ) |
5 |
|
idd |
⊢ ( 𝐴 ∈ On → ( 𝐴 ≠ ∅ → 𝐴 ≠ ∅ ) ) |
6 |
|
idd |
⊢ ( 𝐴 ∈ On → ( ( cf ‘ 𝐴 ) = 𝐴 → ( cf ‘ 𝐴 ) = 𝐴 ) ) |
7 |
|
inawinalem |
⊢ ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) |
8 |
5 6 7
|
3anim123d |
⊢ ( 𝐴 ∈ On → ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) ) |
9 |
4 8
|
mpcom |
⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) |
10 |
|
elina |
⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) ) |
11 |
|
elwina |
⊢ ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) |
12 |
9 10 11
|
3imtr4i |
⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw ) |