Step | Hyp | Ref
| Expression |
1 | | smodm 6270 |
. . . . 5
⊢ (Smo
𝐵 → Ord dom 𝐵) |
2 | | ordtr1 4373 |
. . . . . . 7
⊢ (Ord dom
𝐵 → ((𝐶 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝐵) → 𝐶 ∈ dom 𝐵)) |
3 | 2 | ancomsd 267 |
. . . . . 6
⊢ (Ord dom
𝐵 → ((𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ dom 𝐵)) |
4 | 3 | expdimp 257 |
. . . . 5
⊢ ((Ord dom
𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ dom 𝐵)) |
5 | 1, 4 | sylan 281 |
. . . 4
⊢ ((Smo
𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ dom 𝐵)) |
6 | | df-smo 6265 |
. . . . . 6
⊢ (Smo
𝐵 ↔ (𝐵:dom 𝐵⟶On ∧ Ord dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)))) |
7 | | eleq1 2233 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝑦 ↔ 𝐶 ∈ 𝑦)) |
8 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐶 → (𝐵‘𝑥) = (𝐵‘𝐶)) |
9 | 8 | eleq1d 2239 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐶 → ((𝐵‘𝑥) ∈ (𝐵‘𝑦) ↔ (𝐵‘𝐶) ∈ (𝐵‘𝑦))) |
10 | 7, 9 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐶 → ((𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) ↔ (𝐶 ∈ 𝑦 → (𝐵‘𝐶) ∈ (𝐵‘𝑦)))) |
11 | | eleq2 2234 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (𝐶 ∈ 𝑦 ↔ 𝐶 ∈ 𝐴)) |
12 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝐵‘𝑦) = (𝐵‘𝐴)) |
13 | 12 | eleq2d 2240 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝐵‘𝐶) ∈ (𝐵‘𝑦) ↔ (𝐵‘𝐶) ∈ (𝐵‘𝐴))) |
14 | 11, 13 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → ((𝐶 ∈ 𝑦 → (𝐵‘𝐶) ∈ (𝐵‘𝑦)) ↔ (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
15 | 10, 14 | rspc2v 2847 |
. . . . . . . . 9
⊢ ((𝐶 ∈ dom 𝐵 ∧ 𝐴 ∈ dom 𝐵) → (∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
16 | 15 | ancoms 266 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵) → (∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
17 | 16 | com12 30 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦)) → ((𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵) → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
18 | 17 | 3ad2ant3 1015 |
. . . . . 6
⊢ ((𝐵:dom 𝐵⟶On ∧ Ord dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐵∀𝑦 ∈ dom 𝐵(𝑥 ∈ 𝑦 → (𝐵‘𝑥) ∈ (𝐵‘𝑦))) → ((𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵) → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
19 | 6, 18 | sylbi 120 |
. . . . 5
⊢ (Smo
𝐵 → ((𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵) → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
20 | 19 | expdimp 257 |
. . . 4
⊢ ((Smo
𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐶 ∈ dom 𝐵 → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
21 | 5, 20 | syld 45 |
. . 3
⊢ ((Smo
𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐶 ∈ 𝐴 → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴)))) |
22 | 21 | pm2.43d 50 |
. 2
⊢ ((Smo
𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐶 ∈ 𝐴 → (𝐵‘𝐶) ∈ (𝐵‘𝐴))) |
23 | 22 | 3impia 1195 |
1
⊢ ((Smo
𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐵‘𝐶) ∈ (𝐵‘𝐴)) |