Step | Hyp | Ref
| Expression |
1 | | isof1o 5390 |
. . . 4
⊢ (𝐹 Isom E , E (A, B) →
𝐹:A–1-1-onto→B) |
2 | | f1of 5069 |
. . . 4
⊢ (𝐹:A–1-1-onto→B →
𝐹:A⟶B) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (𝐹 Isom E , E (A, B) →
𝐹:A⟶B) |
4 | | ffdm 5004 |
. . . . . 6
⊢ (𝐹:A⟶B
→ (𝐹:dom 𝐹⟶B ∧ dom 𝐹 ⊆ A)) |
5 | 4 | simpld 105 |
. . . . 5
⊢ (𝐹:A⟶B
→ 𝐹:dom 𝐹⟶B) |
6 | | fss 4997 |
. . . . 5
⊢ ((𝐹:dom 𝐹⟶B ∧ B ⊆ On) → 𝐹:dom 𝐹⟶On) |
7 | 5, 6 | sylan 267 |
. . . 4
⊢ ((𝐹:A⟶B ∧ B ⊆ On)
→ 𝐹:dom 𝐹⟶On) |
8 | 7 | 3adant2 922 |
. . 3
⊢ ((𝐹:A⟶B ∧ Ord A ∧ B ⊆ On)
→ 𝐹:dom 𝐹⟶On) |
9 | 3, 8 | syl3an1 1167 |
. 2
⊢ ((𝐹 Isom E , E (A, B) ∧ Ord A ∧ B ⊆ On)
→ 𝐹:dom 𝐹⟶On) |
10 | | fdm 4993 |
. . . . . 6
⊢ (𝐹:A⟶B
→ dom 𝐹 = A) |
11 | 10 | eqcomd 2042 |
. . . . 5
⊢ (𝐹:A⟶B
→ A = dom 𝐹) |
12 | | ordeq 4075 |
. . . . 5
⊢ (A = dom 𝐹 → (Ord A ↔ Ord dom 𝐹)) |
13 | 1, 2, 11, 12 | 4syl 18 |
. . . 4
⊢ (𝐹 Isom E , E (A, B) →
(Ord A ↔ Ord dom 𝐹)) |
14 | 13 | biimpa 280 |
. . 3
⊢ ((𝐹 Isom E , E (A, B) ∧ Ord A) →
Ord dom 𝐹) |
15 | 14 | 3adant3 923 |
. 2
⊢ ((𝐹 Isom E , E (A, B) ∧ Ord A ∧ B ⊆ On)
→ Ord dom 𝐹) |
16 | 10 | eleq2d 2104 |
. . . . . . 7
⊢ (𝐹:A⟶B
→ (x ∈ dom 𝐹 ↔ x ∈ A)) |
17 | 10 | eleq2d 2104 |
. . . . . . 7
⊢ (𝐹:A⟶B
→ (y ∈ dom 𝐹 ↔ y ∈ A)) |
18 | 16, 17 | anbi12d 442 |
. . . . . 6
⊢ (𝐹:A⟶B
→ ((x ∈ dom 𝐹 ∧ y ∈ dom 𝐹) ↔ (x ∈ A ∧ y ∈ A))) |
19 | 1, 2, 18 | 3syl 17 |
. . . . 5
⊢ (𝐹 Isom E , E (A, B) →
((x ∈ dom
𝐹 ∧ y ∈ dom 𝐹) ↔ (x ∈ A ∧ y ∈ A))) |
20 | | epel 4020 |
. . . . . . . . 9
⊢ (x E y ↔
x ∈
y) |
21 | | isorel 5391 |
. . . . . . . . 9
⊢ ((𝐹 Isom E , E (A, B) ∧ (x ∈ A ∧ y ∈ A)) →
(x E y
↔ (𝐹‘x) E (𝐹‘y))) |
22 | 20, 21 | syl5bbr 183 |
. . . . . . . 8
⊢ ((𝐹 Isom E , E (A, B) ∧ (x ∈ A ∧ y ∈ A)) →
(x ∈
y ↔ (𝐹‘x) E (𝐹‘y))) |
23 | | ffn 4989 |
. . . . . . . . . . 11
⊢ (𝐹:A⟶B
→ 𝐹 Fn A) |
24 | 3, 23 | syl 14 |
. . . . . . . . . 10
⊢ (𝐹 Isom E , E (A, B) →
𝐹 Fn A) |
25 | 24 | adantr 261 |
. . . . . . . . 9
⊢ ((𝐹 Isom E , E (A, B) ∧ (x ∈ A ∧ y ∈ A)) →
𝐹 Fn A) |
26 | | simprr 484 |
. . . . . . . . 9
⊢ ((𝐹 Isom E , E (A, B) ∧ (x ∈ A ∧ y ∈ A)) →
y ∈
A) |
27 | | funfvex 5135 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ y ∈ dom 𝐹) → (𝐹‘y) ∈
V) |
28 | 27 | funfni 4942 |
. . . . . . . . . 10
⊢ ((𝐹 Fn A ∧ y ∈ A) → (𝐹‘y) ∈
V) |
29 | | epelg 4018 |
. . . . . . . . . 10
⊢ ((𝐹‘y) ∈ V →
((𝐹‘x) E (𝐹‘y) ↔ (𝐹‘x) ∈ (𝐹‘y))) |
30 | 28, 29 | syl 14 |
. . . . . . . . 9
⊢ ((𝐹 Fn A ∧ y ∈ A) → ((𝐹‘x) E (𝐹‘y) ↔ (𝐹‘x) ∈ (𝐹‘y))) |
31 | 25, 26, 30 | syl2anc 391 |
. . . . . . . 8
⊢ ((𝐹 Isom E , E (A, B) ∧ (x ∈ A ∧ y ∈ A)) →
((𝐹‘x) E (𝐹‘y) ↔ (𝐹‘x) ∈ (𝐹‘y))) |
32 | 22, 31 | bitrd 177 |
. . . . . . 7
⊢ ((𝐹 Isom E , E (A, B) ∧ (x ∈ A ∧ y ∈ A)) →
(x ∈
y ↔ (𝐹‘x) ∈ (𝐹‘y))) |
33 | 32 | biimpd 132 |
. . . . . 6
⊢ ((𝐹 Isom E , E (A, B) ∧ (x ∈ A ∧ y ∈ A)) →
(x ∈
y → (𝐹‘x) ∈ (𝐹‘y))) |
34 | 33 | ex 108 |
. . . . 5
⊢ (𝐹 Isom E , E (A, B) →
((x ∈
A ∧
y ∈
A) → (x ∈ y → (𝐹‘x) ∈ (𝐹‘y)))) |
35 | 19, 34 | sylbid 139 |
. . . 4
⊢ (𝐹 Isom E , E (A, B) →
((x ∈ dom
𝐹 ∧ y ∈ dom 𝐹) → (x ∈ y → (𝐹‘x) ∈ (𝐹‘y)))) |
36 | 35 | ralrimivv 2394 |
. . 3
⊢ (𝐹 Isom E , E (A, B) →
∀x
∈ dom 𝐹∀y ∈ dom 𝐹(x ∈ y →
(𝐹‘x) ∈ (𝐹‘y))) |
37 | 36 | 3ad2ant1 924 |
. 2
⊢ ((𝐹 Isom E , E (A, B) ∧ Ord A ∧ B ⊆ On)
→ ∀x ∈ dom 𝐹∀y ∈ dom 𝐹(x ∈ y →
(𝐹‘x) ∈ (𝐹‘y))) |
38 | | df-smo 5842 |
. 2
⊢ (Smo
𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀x ∈ dom 𝐹∀y ∈ dom 𝐹(x ∈ y →
(𝐹‘x) ∈ (𝐹‘y)))) |
39 | 9, 15, 37, 38 | syl3anbrc 1087 |
1
⊢ ((𝐹 Isom E , E (A, B) ∧ Ord A ∧ B ⊆ On)
→ Smo 𝐹) |