Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐶 = ∅) |
2 | 1 | oveq1d 6939 |
. . . . . . 7
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶 ↑𝑚 𝐴) = (∅
↑𝑚 𝐴)) |
3 | | simplr 759 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) |
4 | | idd 24 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → 𝐴 = ∅)) |
5 | 4, 1 | jctird 522 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐴 = ∅ → (𝐴 = ∅ ∧ 𝐶 = ∅))) |
6 | 3, 5 | mtod 190 |
. . . . . . . . 9
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → ¬ 𝐴 = ∅) |
7 | 6 | neqned 2976 |
. . . . . . . 8
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → 𝐴 ≠ ∅) |
8 | | map0b 8183 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ → (∅
↑𝑚 𝐴) = ∅) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (∅
↑𝑚 𝐴) = ∅) |
10 | 2, 9 | eqtrd 2814 |
. . . . . 6
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶 ↑𝑚 𝐴) = ∅) |
11 | | ovex 6956 |
. . . . . . 7
⊢ (𝐶 ↑𝑚
𝐵) ∈
V |
12 | 11 | 0dom 8380 |
. . . . . 6
⊢ ∅
≼ (𝐶
↑𝑚 𝐵) |
13 | 10, 12 | syl6eqbr 4927 |
. . . . 5
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 = ∅) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |
14 | | simpll 757 |
. . . . . . . 8
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐴 ≼ 𝐵) |
15 | | reldom 8249 |
. . . . . . . . . . 11
⊢ Rel
≼ |
16 | 15 | brrelex2i 5409 |
. . . . . . . . . 10
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
17 | 16 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → 𝐵 ∈ V) |
18 | | domeng 8257 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
20 | 14, 19 | mpbid 224 |
. . . . . . 7
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
21 | | enrefg 8275 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ V → 𝐶 ≈ 𝐶) |
22 | 21 | ad2antlr 717 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐶 ≈ 𝐶) |
23 | | simprrl 771 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐴 ≈ 𝑥) |
24 | | mapen 8414 |
. . . . . . . . . . 11
⊢ ((𝐶 ≈ 𝐶 ∧ 𝐴 ≈ 𝑥) → (𝐶 ↑𝑚 𝐴) ≈ (𝐶 ↑𝑚 𝑥)) |
25 | 22, 23, 24 | syl2anc 579 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 𝐴) ≈ (𝐶 ↑𝑚 𝑥)) |
26 | | ovexd 6958 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 𝑥) ∈ V) |
27 | | ovexd 6958 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 (𝐵 ∖ 𝑥)) ∈ V) |
28 | | simprl 761 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐶 ≠ ∅) |
29 | | simplr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐶 ∈ V) |
30 | 16 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝐵 ∈ V) |
31 | | difexg 5047 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ V → (𝐵 ∖ 𝑥) ∈ V) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐵 ∖ 𝑥) ∈ V) |
33 | | map0g 8184 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V) → ((𝐶 ↑𝑚 (𝐵 ∖ 𝑥)) = ∅ ↔ (𝐶 = ∅ ∧ (𝐵 ∖ 𝑥) ≠ ∅))) |
34 | | simpl 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 = ∅ ∧ (𝐵 ∖ 𝑥) ≠ ∅) → 𝐶 = ∅) |
35 | 33, 34 | syl6bi 245 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V) → ((𝐶 ↑𝑚 (𝐵 ∖ 𝑥)) = ∅ → 𝐶 = ∅)) |
36 | 35 | necon3d 2990 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V) → (𝐶 ≠ ∅ → (𝐶 ↑𝑚 (𝐵 ∖ 𝑥)) ≠ ∅)) |
37 | 29, 32, 36 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ≠ ∅ → (𝐶 ↑𝑚 (𝐵 ∖ 𝑥)) ≠ ∅)) |
38 | 28, 37 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 (𝐵 ∖ 𝑥)) ≠ ∅) |
39 | | xpdom3 8348 |
. . . . . . . . . . . 12
⊢ (((𝐶 ↑𝑚
𝑥) ∈ V ∧ (𝐶 ↑𝑚
(𝐵 ∖ 𝑥)) ∈ V ∧ (𝐶 ↑𝑚
(𝐵 ∖ 𝑥)) ≠ ∅) → (𝐶 ↑𝑚
𝑥) ≼ ((𝐶 ↑𝑚
𝑥) × (𝐶 ↑𝑚
(𝐵 ∖ 𝑥)))) |
40 | 26, 27, 38, 39 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 𝑥) ≼ ((𝐶 ↑𝑚 𝑥) × (𝐶 ↑𝑚 (𝐵 ∖ 𝑥)))) |
41 | | vex 3401 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝑥 ∈ V) |
43 | | disjdif 4264 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∩ (𝐵 ∖ 𝑥)) = ∅ |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝑥 ∩ (𝐵 ∖ 𝑥)) = ∅) |
45 | | mapunen 8419 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ V ∧ (𝐵 ∖ 𝑥) ∈ V ∧ 𝐶 ∈ V) ∧ (𝑥 ∩ (𝐵 ∖ 𝑥)) = ∅) → (𝐶 ↑𝑚 (𝑥 ∪ (𝐵 ∖ 𝑥))) ≈ ((𝐶 ↑𝑚 𝑥) × (𝐶 ↑𝑚 (𝐵 ∖ 𝑥)))) |
46 | 42, 32, 29, 44, 45 | syl31anc 1441 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 (𝑥 ∪ (𝐵 ∖ 𝑥))) ≈ ((𝐶 ↑𝑚 𝑥) × (𝐶 ↑𝑚 (𝐵 ∖ 𝑥)))) |
47 | 46 | ensymd 8294 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → ((𝐶 ↑𝑚 𝑥) × (𝐶 ↑𝑚 (𝐵 ∖ 𝑥))) ≈ (𝐶 ↑𝑚 (𝑥 ∪ (𝐵 ∖ 𝑥)))) |
48 | | simprrr 772 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → 𝑥 ⊆ 𝐵) |
49 | | undif 4273 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝐵 ↔ (𝑥 ∪ (𝐵 ∖ 𝑥)) = 𝐵) |
50 | 48, 49 | sylib 210 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝑥 ∪ (𝐵 ∖ 𝑥)) = 𝐵) |
51 | 50 | oveq2d 6940 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 (𝑥 ∪ (𝐵 ∖ 𝑥))) = (𝐶 ↑𝑚 𝐵)) |
52 | 47, 51 | breqtrd 4914 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → ((𝐶 ↑𝑚 𝑥) × (𝐶 ↑𝑚 (𝐵 ∖ 𝑥))) ≈ (𝐶 ↑𝑚 𝐵)) |
53 | | domentr 8302 |
. . . . . . . . . . 11
⊢ (((𝐶 ↑𝑚
𝑥) ≼ ((𝐶 ↑𝑚
𝑥) × (𝐶 ↑𝑚
(𝐵 ∖ 𝑥))) ∧ ((𝐶 ↑𝑚 𝑥) × (𝐶 ↑𝑚 (𝐵 ∖ 𝑥))) ≈ (𝐶 ↑𝑚 𝐵)) → (𝐶 ↑𝑚 𝑥) ≼ (𝐶 ↑𝑚 𝐵)) |
54 | 40, 52, 53 | syl2anc 579 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 𝑥) ≼ (𝐶 ↑𝑚 𝐵)) |
55 | | endomtr 8301 |
. . . . . . . . . 10
⊢ (((𝐶 ↑𝑚
𝐴) ≈ (𝐶 ↑𝑚
𝑥) ∧ (𝐶 ↑𝑚 𝑥) ≼ (𝐶 ↑𝑚 𝐵)) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |
56 | 25, 54, 55 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ (𝐶 ≠ ∅ ∧ (𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |
57 | 56 | expr 450 |
. . . . . . . 8
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → ((𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵))) |
58 | 57 | exlimdv 1976 |
. . . . . . 7
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵))) |
59 | 20, 58 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ 𝐶 ≠ ∅) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |
60 | 59 | adantlr 705 |
. . . . 5
⊢ ((((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ≠ ∅) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |
61 | 13, 60 | pm2.61dane 3057 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |
62 | 61 | an32s 642 |
. . 3
⊢ (((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) ∧ 𝐶 ∈ V) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |
63 | 62 | ex 403 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ∈ V → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵))) |
64 | | reldmmap 8151 |
. . . 4
⊢ Rel dom
↑𝑚 |
65 | 64 | ovprc1 6962 |
. . 3
⊢ (¬
𝐶 ∈ V → (𝐶 ↑𝑚
𝐴) =
∅) |
66 | 65, 12 | syl6eqbr 4927 |
. 2
⊢ (¬
𝐶 ∈ V → (𝐶 ↑𝑚
𝐴) ≼ (𝐶 ↑𝑚
𝐵)) |
67 | 63, 66 | pm2.61d1 173 |
1
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) |