Step | Hyp | Ref
| Expression |
1 | | reldom 7847 |
. . . . . . 7
⊢ Rel
≼ |
2 | 1 | brrelex2i 5083 |
. . . . . 6
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
3 | | domeng 7855 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
5 | 4 | ibi 255 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
6 | 5 | adantr 480 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
7 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵) → 𝐴 ≈ 𝑥) |
8 | | enrefg 7873 |
. . . . . 6
⊢ (𝐶 ∈ V → 𝐶 ≈ 𝐶) |
9 | 8 | adantl 481 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → 𝐶 ≈ 𝐶) |
10 | | mapen 8009 |
. . . . 5
⊢ ((𝐴 ≈ 𝑥 ∧ 𝐶 ≈ 𝐶) → (𝐴 ↑𝑚 𝐶) ≈ (𝑥 ↑𝑚 𝐶)) |
11 | 7, 9, 10 | syl2anr 494 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝐴 ↑𝑚 𝐶) ≈ (𝑥 ↑𝑚 𝐶)) |
12 | | ovex 6577 |
. . . . 5
⊢ (𝐵 ↑𝑚
𝐶) ∈
V |
13 | 2 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → 𝐵 ∈ V) |
14 | | simprr 792 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → 𝑥 ⊆ 𝐵) |
15 | | mapss 7786 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑥 ⊆ 𝐵) → (𝑥 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
16 | 13, 14, 15 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝑥 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
17 | | ssdomg 7887 |
. . . . 5
⊢ ((𝐵 ↑𝑚
𝐶) ∈ V → ((𝑥 ↑𝑚
𝐶) ⊆ (𝐵 ↑𝑚
𝐶) → (𝑥 ↑𝑚
𝐶) ≼ (𝐵 ↑𝑚
𝐶))) |
18 | 12, 16, 17 | mpsyl 66 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝑥 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
19 | | endomtr 7900 |
. . . 4
⊢ (((𝐴 ↑𝑚
𝐶) ≈ (𝑥 ↑𝑚
𝐶) ∧ (𝑥 ↑𝑚
𝐶) ≼ (𝐵 ↑𝑚
𝐶)) → (𝐴 ↑𝑚
𝐶) ≼ (𝐵 ↑𝑚
𝐶)) |
20 | 11, 18, 19 | syl2anc 691 |
. . 3
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
21 | 6, 20 | exlimddv 1850 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
22 | | elmapex 7764 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ↑𝑚 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
23 | 22 | simprd 478 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ↑𝑚 𝐶) → 𝐶 ∈ V) |
24 | 23 | con3i 149 |
. . . . 5
⊢ (¬
𝐶 ∈ V → ¬
𝑥 ∈ (𝐴 ↑𝑚 𝐶)) |
25 | 24 | eq0rdv 3931 |
. . . 4
⊢ (¬
𝐶 ∈ V → (𝐴 ↑𝑚
𝐶) =
∅) |
26 | 25 | adantl 481 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 ↑𝑚 𝐶) = ∅) |
27 | 12 | 0dom 7975 |
. . 3
⊢ ∅
≼ (𝐵
↑𝑚 𝐶) |
28 | 26, 27 | syl6eqbr 4622 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
29 | 21, 28 | pm2.61dan 828 |
1
⊢ (𝐴 ≼ 𝐵 → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |