| Step | Hyp | Ref
| Expression |
| 1 | | reldom 8991 |
. . . . . . 7
⊢ Rel
≼ |
| 2 | 1 | brrelex2i 5742 |
. . . . . 6
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
| 3 | | domeng 9003 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
| 4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
| 5 | 4 | ibi 267 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
| 6 | 5 | adantr 480 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
| 7 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵) → 𝐴 ≈ 𝑥) |
| 8 | | enrefg 9024 |
. . . . . 6
⊢ (𝐶 ∈ V → 𝐶 ≈ 𝐶) |
| 9 | 8 | adantl 481 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → 𝐶 ≈ 𝐶) |
| 10 | | mapen 9181 |
. . . . 5
⊢ ((𝐴 ≈ 𝑥 ∧ 𝐶 ≈ 𝐶) → (𝐴 ↑m 𝐶) ≈ (𝑥 ↑m 𝐶)) |
| 11 | 7, 9, 10 | syl2anr 597 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝐴 ↑m 𝐶) ≈ (𝑥 ↑m 𝐶)) |
| 12 | | ovex 7464 |
. . . . 5
⊢ (𝐵 ↑m 𝐶) ∈ V |
| 13 | 2 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → 𝐵 ∈ V) |
| 14 | | simprr 773 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → 𝑥 ⊆ 𝐵) |
| 15 | | mapss 8929 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑥 ⊆ 𝐵) → (𝑥 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) |
| 16 | 13, 14, 15 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝑥 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) |
| 17 | | ssdomg 9040 |
. . . . 5
⊢ ((𝐵 ↑m 𝐶) ∈ V → ((𝑥 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶) → (𝑥 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶))) |
| 18 | 12, 16, 17 | mpsyl 68 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝑥 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) |
| 19 | | endomtr 9052 |
. . . 4
⊢ (((𝐴 ↑m 𝐶) ≈ (𝑥 ↑m 𝐶) ∧ (𝑥 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) → (𝐴 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) |
| 20 | 11, 18, 19 | syl2anc 584 |
. . 3
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) → (𝐴 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) |
| 21 | 6, 20 | exlimddv 1935 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → (𝐴 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) |
| 22 | | elmapex 8888 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ↑m 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
| 23 | 22 | simprd 495 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ↑m 𝐶) → 𝐶 ∈ V) |
| 24 | 23 | con3i 154 |
. . . . 5
⊢ (¬
𝐶 ∈ V → ¬
𝑥 ∈ (𝐴 ↑m 𝐶)) |
| 25 | 24 | eq0rdv 4407 |
. . . 4
⊢ (¬
𝐶 ∈ V → (𝐴 ↑m 𝐶) = ∅) |
| 26 | 25 | adantl 481 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 ↑m 𝐶) = ∅) |
| 27 | 12 | 0dom 9146 |
. . 3
⊢ ∅
≼ (𝐵
↑m 𝐶) |
| 28 | 26, 27 | eqbrtrdi 5182 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) |
| 29 | 21, 28 | pm2.61dan 813 |
1
⊢ (𝐴 ≼ 𝐵 → (𝐴 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) |