| Step | Hyp | Ref
| Expression |
| 1 | | isof1o 7343 |
. . . 4
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵) |
| 2 | | f1of 6848 |
. . . 4
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴⟶𝐵) |
| 4 | | ffdm 6765 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴)) |
| 5 | 4 | simpld 494 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:dom 𝐹⟶𝐵) |
| 6 | | fss 6752 |
. . . . 5
⊢ ((𝐹:dom 𝐹⟶𝐵 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On) |
| 7 | 5, 6 | sylan 580 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On) |
| 8 | 7 | 3adant2 1132 |
. . 3
⊢ ((𝐹:𝐴⟶𝐵 ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On) |
| 9 | 3, 8 | syl3an1 1164 |
. 2
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On) |
| 10 | | fdm 6745 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
| 11 | 10 | eqcomd 2743 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = dom 𝐹) |
| 12 | | ordeq 6391 |
. . . . 5
⊢ (𝐴 = dom 𝐹 → (Ord 𝐴 ↔ Ord dom 𝐹)) |
| 13 | 1, 2, 11, 12 | 4syl 19 |
. . . 4
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → (Ord 𝐴 ↔ Ord dom 𝐹)) |
| 14 | 13 | biimpa 476 |
. . 3
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴) → Ord dom 𝐹) |
| 15 | 14 | 3adant3 1133 |
. 2
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Ord dom 𝐹) |
| 16 | 10 | eleq2d 2827 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
| 17 | 10 | eleq2d 2827 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴)) |
| 18 | 16, 17 | anbi12d 632 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))) |
| 19 | 1, 2, 18 | 3syl 18 |
. . . . 5
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))) |
| 20 | | isorel 7346 |
. . . . . . . 8
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 E 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦))) |
| 21 | | epel 5587 |
. . . . . . . 8
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
| 22 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘𝑦) ∈ V |
| 23 | 22 | epeli 5586 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) E (𝐹‘𝑦) ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦)) |
| 24 | 20, 21, 23 | 3bitr3g 313 |
. . . . . . 7
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦))) |
| 25 | 24 | biimpd 229 |
. . . . . 6
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦))) |
| 26 | 25 | ex 412 |
. . . . 5
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦)))) |
| 27 | 19, 26 | sylbid 240 |
. . . 4
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦)))) |
| 28 | 27 | ralrimivv 3200 |
. . 3
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹(𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦))) |
| 29 | 28 | 3ad2ant1 1134 |
. 2
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹(𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦))) |
| 30 | | df-smo 8386 |
. 2
⊢ (Smo
𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹(𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦)))) |
| 31 | 9, 15, 29, 30 | syl3anbrc 1344 |
1
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹) |