Step | Hyp | Ref
| Expression |
1 | | reldom 7961 |
. . . . . . 7
⊢ Rel
≼ |
2 | 1 | brrelex2i 5159 |
. . . . . 6
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
3 | | domeng 7969 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
5 | 4 | ibi 256 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
6 | 5 | adantr 481 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
7 | | simpl 473 |
. . . . 5
⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵) → 𝐴 ≈ 𝑥) |
8 | | enrefg 7987 |
. . . . . 6
⊢ (𝐶 ∈ V → 𝐶 ≈ 𝐶) |
9 | 8 | adantl 482 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → 𝐶 ≈ 𝐶) |
10 | | mapen 8124 |
. . . . 5
⊢ ((𝐴 ≈ 𝑥 ∧ 𝐶 ≈ 𝐶) → (𝐴 ↑𝑚 𝐶) ≈ (𝑥 ↑𝑚 𝐶)) |
11 | 7, 9, 10 | syl2anr 495 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝐴 ↑𝑚 𝐶) ≈ (𝑥 ↑𝑚 𝐶)) |
12 | | ovex 6678 |
. . . . 5
⊢ (𝐵 ↑𝑚
𝐶) ∈
V |
13 | 2 | ad2antrr 762 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → 𝐵 ∈ V) |
14 | | simprr 796 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → 𝑥 ⊆ 𝐵) |
15 | | mapss 7900 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑥 ⊆ 𝐵) → (𝑥 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
16 | 13, 14, 15 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝑥 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
17 | | ssdomg 8001 |
. . . . 5
⊢ ((𝐵 ↑𝑚
𝐶) ∈ V → ((𝑥 ↑𝑚
𝐶) ⊆ (𝐵 ↑𝑚
𝐶) → (𝑥 ↑𝑚
𝐶) ≼ (𝐵 ↑𝑚
𝐶))) |
18 | 12, 16, 17 | mpsyl 68 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝑥 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
19 | | endomtr 8014 |
. . . 4
⊢ (((𝐴 ↑𝑚
𝐶) ≈ (𝑥 ↑𝑚
𝐶) ∧ (𝑥 ↑𝑚
𝐶) ≼ (𝐵 ↑𝑚
𝐶)) → (𝐴 ↑𝑚
𝐶) ≼ (𝐵 ↑𝑚
𝐶)) |
20 | 11, 18, 19 | syl2anc 693 |
. . 3
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
21 | 6, 20 | exlimddv 1863 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
22 | | elmapex 7878 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ↑𝑚 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
23 | 22 | simprd 479 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ↑𝑚 𝐶) → 𝐶 ∈ V) |
24 | 23 | con3i 150 |
. . . . 5
⊢ (¬
𝐶 ∈ V → ¬
𝑥 ∈ (𝐴 ↑𝑚 𝐶)) |
25 | 24 | eq0rdv 3979 |
. . . 4
⊢ (¬
𝐶 ∈ V → (𝐴 ↑𝑚
𝐶) =
∅) |
26 | 25 | adantl 482 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 ↑𝑚 𝐶) = ∅) |
27 | 12 | 0dom 8090 |
. . 3
⊢ ∅
≼ (𝐵
↑𝑚 𝐶) |
28 | 26, 27 | syl6eqbr 4692 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
29 | 21, 28 | pm2.61dan 832 |
1
⊢ (𝐴 ≼ 𝐵 → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |