Step |
Hyp |
Ref |
Expression |
1 |
|
isof1o |
⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) |
2 |
|
f1of |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
3 |
1 2
|
syl |
⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
4 |
|
ffdm |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) ) |
5 |
4
|
simpld |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : dom 𝐹 ⟶ 𝐵 ) |
6 |
|
fss |
⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ 𝐵 ⊆ On ) → 𝐹 : dom 𝐹 ⟶ On ) |
7 |
5 6
|
sylan |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ On ) → 𝐹 : dom 𝐹 ⟶ On ) |
8 |
7
|
3adant2 |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → 𝐹 : dom 𝐹 ⟶ On ) |
9 |
3 8
|
syl3an1 |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → 𝐹 : dom 𝐹 ⟶ On ) |
10 |
|
fdm |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 ) |
11 |
10
|
eqcomd |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 = dom 𝐹 ) |
12 |
|
ordeq |
⊢ ( 𝐴 = dom 𝐹 → ( Ord 𝐴 ↔ Ord dom 𝐹 ) ) |
13 |
1 2 11 12
|
4syl |
⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ( Ord 𝐴 ↔ Ord dom 𝐹 ) ) |
14 |
13
|
biimpa |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ) → Ord dom 𝐹 ) |
15 |
14
|
3adant3 |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → Ord dom 𝐹 ) |
16 |
10
|
eleq2d |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) ) |
17 |
10
|
eleq2d |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴 ) ) |
18 |
16 17
|
anbi12d |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ) |
19 |
1 2 18
|
3syl |
⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ) |
20 |
|
isorel |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 E 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ) ) |
21 |
|
epel |
⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 ) |
22 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑦 ) ∈ V |
23 |
22
|
epeli |
⊢ ( ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) |
24 |
20 21 23
|
3bitr3g |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) |
25 |
24
|
biimpd |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) |
26 |
25
|
ex |
⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ) |
27 |
19 26
|
sylbid |
⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑥 ∈ 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ) |
28 |
27
|
ralrimivv |
⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ∈ 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) |
29 |
28
|
3ad2ant1 |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ∈ 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) |
30 |
|
df-smo |
⊢ ( Smo 𝐹 ↔ ( 𝐹 : dom 𝐹 ⟶ On ∧ Ord dom 𝐹 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ∈ 𝑦 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ) |
31 |
9 15 29 30
|
syl3anbrc |
⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → Smo 𝐹 ) |