| Step | Hyp | Ref
| Expression |
| 1 | | fof 6820 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
| 2 | | smo11 8404 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹) → 𝐹:𝐴–1-1→𝐵) |
| 3 | 1, 2 | sylan 580 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) → 𝐹:𝐴–1-1→𝐵) |
| 4 | | simpl 482 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) → 𝐹:𝐴–onto→𝐵) |
| 5 | | df-f1o 6568 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
| 6 | 3, 4, 5 | sylanbrc 583 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) → 𝐹:𝐴–1-1-onto→𝐵) |
| 7 | 6 | adantl 481 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ On) ∧ (𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹)) → 𝐹:𝐴–1-1-onto→𝐵) |
| 8 | | fofn 6822 |
. . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
| 9 | | smoord 8405 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦))) |
| 10 | | epel 5587 |
. . . . . . . 8
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
| 11 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘𝑦) ∈ V |
| 12 | 11 | epeli 5586 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) E (𝐹‘𝑦) ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦)) |
| 13 | 9, 10, 12 | 3bitr4g 314 |
. . . . . . 7
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 E 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦))) |
| 14 | 13 | ralrimivva 3202 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 E 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦))) |
| 15 | 8, 14 | sylan 580 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 E 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦))) |
| 16 | 15 | adantl 481 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ On) ∧ (𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 E 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦))) |
| 17 | | df-isom 6570 |
. . . 4
⊢ (𝐹 Isom E , E (𝐴, 𝐵) ↔ (𝐹:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 E 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦)))) |
| 18 | 7, 16, 17 | sylanbrc 583 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐵 ⊆ On) ∧ (𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹)) → 𝐹 Isom E , E (𝐴, 𝐵)) |
| 19 | 18 | ex 412 |
. 2
⊢ ((Ord
𝐴 ∧ 𝐵 ⊆ On) → ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) → 𝐹 Isom E , E (𝐴, 𝐵))) |
| 20 | | isof1o 7343 |
. . . . . . 7
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵) |
| 21 | | f1ofo 6855 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
| 22 | 20, 21 | syl 17 |
. . . . . 6
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–onto→𝐵) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → 𝐹:𝐴–onto→𝐵) |
| 24 | | smoiso 8402 |
. . . . 5
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹) |
| 25 | 23, 24 | jca 511 |
. . . 4
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → (𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹)) |
| 26 | 25 | 3expib 1123 |
. . 3
⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ((Ord 𝐴 ∧ 𝐵 ⊆ On) → (𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹))) |
| 27 | 26 | com12 32 |
. 2
⊢ ((Ord
𝐴 ∧ 𝐵 ⊆ On) → (𝐹 Isom E , E (𝐴, 𝐵) → (𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹))) |
| 28 | 19, 27 | impbid 212 |
1
⊢ ((Ord
𝐴 ∧ 𝐵 ⊆ On) → ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (𝐴, 𝐵))) |