Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) |
2 | | dmeq 4535 |
. . . 4
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) |
3 | 1, 2 | feq12d 5036 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐴:dom 𝐴⟶On ↔ 𝐵:dom 𝐵⟶On)) |
4 | | ordeq 4109 |
. . . 4
⊢ (dom
𝐴 = dom 𝐵 → (Ord dom 𝐴 ↔ Ord dom 𝐵)) |
5 | 2, 4 | syl 14 |
. . 3
⊢ (𝐴 = 𝐵 → (Ord dom 𝐴 ↔ Ord dom 𝐵)) |
6 | | fveq1 5177 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴‘𝑥) = (𝐵‘𝑥)) |
7 | | fveq1 5177 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴‘𝑦) = (𝐵‘𝑦)) |
8 | 6, 7 | eleq12d 2108 |
. . . . . 6
⊢ (𝐴 = 𝐵 → ((𝐴‘𝑥) ∈ (𝐴‘𝑦) ↔ (𝐵‘𝑥) ∈ (𝐵‘𝑦))) |
9 | 8 | imbi2d 219 |
. . . . 5
⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) ↔ (𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
10 | 9 | 2ralbidv 2348 |
. . . 4
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
11 | 2 | raleqdv 2511 |
. . . . 5
⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) ↔ ∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
12 | 11 | ralbidv 2326 |
. . . 4
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
13 | 2 | raleqdv 2511 |
. . . 4
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
14 | 10, 12, 13 | 3bitrd 203 |
. . 3
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) ↔ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
15 | 3, 5, 14 | 3anbi123d 1207 |
. 2
⊢ (𝐴 = 𝐵 → ((𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) ↔ (𝐵:dom 𝐵⟶On ∧ Ord dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦))))) |
16 | | df-smo 5901 |
. 2
⊢ (Smo
𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
17 | | df-smo 5901 |
. 2
⊢ (Smo
𝐵 ↔ (𝐵:dom 𝐵⟶On ∧ Ord dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
18 | 15, 16, 17 | 3bitr4g 212 |
1
⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵)) |