Step |
Hyp |
Ref |
Expression |
0 |
|
cA |
⊢ 𝐴 |
1 |
0
|
wsmo |
⊢ Smo 𝐴 |
2 |
0
|
cdm |
⊢ dom 𝐴 |
3 |
|
con0 |
⊢ On |
4 |
2 3 0
|
wf |
⊢ 𝐴 : dom 𝐴 ⟶ On |
5 |
2
|
word |
⊢ Ord dom 𝐴 |
6 |
|
vx |
⊢ 𝑥 |
7 |
|
vy |
⊢ 𝑦 |
8 |
6
|
cv |
⊢ 𝑥 |
9 |
7
|
cv |
⊢ 𝑦 |
10 |
8 9
|
wcel |
⊢ 𝑥 ∈ 𝑦 |
11 |
8 0
|
cfv |
⊢ ( 𝐴 ‘ 𝑥 ) |
12 |
9 0
|
cfv |
⊢ ( 𝐴 ‘ 𝑦 ) |
13 |
11 12
|
wcel |
⊢ ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) |
14 |
10 13
|
wi |
⊢ ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) |
15 |
14 7 2
|
wral |
⊢ ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) |
16 |
15 6 2
|
wral |
⊢ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) |
17 |
4 5 16
|
w3a |
⊢ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) |
18 |
1 17
|
wb |
⊢ ( Smo 𝐴 ↔ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) ) |