Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. . . . . . . 8
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐶 = ∅) |
2 | 1 | oveq1d 7173 |
. . . . . . 7
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶 ↑m 𝐴) = (∅ ↑m 𝐴)) |
3 | | simplr 767 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) |
4 | | idd 24 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → 𝐴 = ∅)) |
5 | 4, 1 | jctird 529 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → (𝐴 = ∅ ∧ 𝐶 = ∅))) |
6 | 3, 5 | mtod 200 |
. . . . . . . . 9
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ 𝐴 = ∅) |
7 | 6 | neqned 3025 |
. . . . . . . 8
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐴 ≠ ∅) |
8 | | map0b 8449 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ → (∅
↑m 𝐴) =
∅) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (∅
↑m 𝐴) =
∅) |
10 | 2, 9 | eqtrd 2858 |
. . . . . 6
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶 ↑m 𝐴) = ∅) |
11 | | ovex 7191 |
. . . . . . 7
⊢ (𝐶 ↑m 𝐵) ∈ V |
12 | 11 | 0dom 8649 |
. . . . . 6
⊢ ∅
≼ (𝐶
↑m 𝐵) |
13 | 10, 12 | eqbrtrdi 5107 |
. . . . 5
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
14 | | simpll 765 |
. . . . . . . 8
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐴 ≼ 𝐵) |
15 | | reldom 8517 |
. . . . . . . . . . 11
⊢ Rel
≼ |
16 | 15 | brrelex2i 5611 |
. . . . . . . . . 10
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
17 | 16 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐵 ∈ V) |
18 | | domeng 8525 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
20 | 14, 19 | mpbid 234 |
. . . . . . 7
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
21 | | enrefg 8543 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ V → 𝐶 ≈ 𝐶) |
22 | 21 | ad2antlr 725 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐶 ≈ 𝐶) |
23 | | simprrl 779 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐴 ≈ 𝑥) |
24 | | mapen 8683 |
. . . . . . . . . . 11
⊢ ((𝐶 ≈ 𝐶 ∧ 𝐴 ≈ 𝑥) → (𝐶 ↑m 𝐴) ≈ (𝐶 ↑m 𝑥)) |
25 | 22, 23, 24 | syl2anc 586 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m 𝐴) ≈ (𝐶 ↑m 𝑥)) |
26 | | ovexd 7193 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m 𝑥) ∈ V) |
27 | | ovexd 7193 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m (𝐵 ∖ 𝑥)) ∈ V) |
28 | | simprl 769 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐶 ≠ ∅) |
29 | | simplr 767 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐶 ∈ V) |
30 | 16 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐵 ∈ V) |
31 | | difexg 5233 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ V → (𝐵 ∖ 𝑥) ∈ V) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐵 ∖ 𝑥) ∈ V) |
33 | | map0g 8450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V) → ((𝐶 ↑m (𝐵 ∖ 𝑥)) = ∅ ↔ (𝐶 = ∅ ∧ (𝐵 ∖ 𝑥) ≠ ∅))) |
34 | | simpl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 = ∅ ∧ (𝐵 ∖ 𝑥) ≠ ∅) → 𝐶 = ∅) |
35 | 33, 34 | syl6bi 255 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V) → ((𝐶 ↑m (𝐵 ∖ 𝑥)) = ∅ → 𝐶 = ∅)) |
36 | 35 | necon3d 3039 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V) → (𝐶 ≠ ∅ → (𝐶 ↑m (𝐵 ∖ 𝑥)) ≠ ∅)) |
37 | 29, 32, 36 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ≠ ∅ → (𝐶 ↑m (𝐵 ∖ 𝑥)) ≠ ∅)) |
38 | 28, 37 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m (𝐵 ∖ 𝑥)) ≠ ∅) |
39 | | xpdom3 8617 |
. . . . . . . . . . . 12
⊢ (((𝐶 ↑m 𝑥) ∈ V ∧ (𝐶 ↑m (𝐵 ∖ 𝑥)) ∈ V ∧ (𝐶 ↑m (𝐵 ∖ 𝑥)) ≠ ∅) → (𝐶 ↑m 𝑥) ≼ ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥)))) |
40 | 26, 27, 38, 39 | syl3anc 1367 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m 𝑥) ≼ ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥)))) |
41 | | vex 3499 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝑥 ∈ V) |
43 | | disjdif 4423 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∩ (𝐵 ∖ 𝑥)) = ∅ |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝑥 ∩ (𝐵 ∖ 𝑥)) = ∅) |
45 | | mapunen 8688 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V ∧ 𝐶 ∈ V) ∧ (𝑥 ∩ (𝐵 ∖ 𝑥)) = ∅) → (𝐶 ↑m (𝑥 ∪ (𝐵 ∖ 𝑥))) ≈ ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥)))) |
46 | 42, 32, 29, 44, 45 | syl31anc 1369 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m (𝑥 ∪ (𝐵 ∖ 𝑥))) ≈ ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥)))) |
47 | 46 | ensymd 8562 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥))) ≈ (𝐶 ↑m (𝑥 ∪ (𝐵 ∖ 𝑥)))) |
48 | | simprrr 780 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝑥 ⊆ 𝐵) |
49 | | undif 4432 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝐵 ↔ (𝑥 ∪ (𝐵 ∖ 𝑥)) = 𝐵) |
50 | 48, 49 | sylib 220 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝑥 ∪ (𝐵 ∖ 𝑥)) = 𝐵) |
51 | 50 | oveq2d 7174 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m (𝑥 ∪ (𝐵 ∖ 𝑥))) = (𝐶 ↑m 𝐵)) |
52 | 47, 51 | breqtrd 5094 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥))) ≈ (𝐶 ↑m 𝐵)) |
53 | | domentr 8570 |
. . . . . . . . . . 11
⊢ (((𝐶 ↑m 𝑥) ≼ ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥))) ∧ ((𝐶 ↑m 𝑥) × (𝐶 ↑m (𝐵 ∖ 𝑥))) ≈ (𝐶 ↑m 𝐵)) → (𝐶 ↑m 𝑥) ≼ (𝐶 ↑m 𝐵)) |
54 | 40, 52, 53 | syl2anc 586 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m 𝑥) ≼ (𝐶 ↑m 𝐵)) |
55 | | endomtr 8569 |
. . . . . . . . . 10
⊢ (((𝐶 ↑m 𝐴) ≈ (𝐶 ↑m 𝑥) ∧ (𝐶 ↑m 𝑥) ≼ (𝐶 ↑m 𝐵)) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
56 | 25, 54, 55 | syl2anc 586 |
. . . . . . . . 9
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
57 | 56 | expr 459 |
. . . . . . . 8
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ((𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵))) |
58 | 57 | exlimdv 1934 |
. . . . . . 7
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵))) |
59 | 20, 58 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
60 | 59 | adantlr 713 |
. . . . 5
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ≠ ∅) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
61 | 13, 60 | pm2.61dane 3106 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
62 | 61 | an32s 650 |
. . 3
⊢ (((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ∈ V) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
63 | 62 | ex 415 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ∈ V → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵))) |
64 | | reldmmap 8417 |
. . . 4
⊢ Rel dom
↑m |
65 | 64 | ovprc1 7197 |
. . 3
⊢ (¬
𝐶 ∈ V → (𝐶 ↑m 𝐴) = ∅) |
66 | 65, 12 | eqbrtrdi 5107 |
. 2
⊢ (¬
𝐶 ∈ V → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |
67 | 63, 66 | pm2.61d1 182 |
1
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) |