Proof of Theorem cdadom1
Step | Hyp | Ref
| Expression |
1 | | snex 4908 |
. . . . 5
⊢ {∅}
∈ V |
2 | 1 | xpdom1 8059 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → (𝐴 × {∅}) ≼ (𝐵 ×
{∅})) |
3 | | snex 4908 |
. . . . . 6
⊢
{1𝑜} ∈ V |
4 | | xpexg 6960 |
. . . . . 6
⊢ ((𝐶 ∈ V ∧
{1𝑜} ∈ V) → (𝐶 × {1𝑜}) ∈
V) |
5 | 3, 4 | mpan2 707 |
. . . . 5
⊢ (𝐶 ∈ V → (𝐶 ×
{1𝑜}) ∈ V) |
6 | | domrefg 7990 |
. . . . 5
⊢ ((𝐶 ×
{1𝑜}) ∈ V → (𝐶 × {1𝑜}) ≼
(𝐶 ×
{1𝑜})) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝐶 ∈ V → (𝐶 ×
{1𝑜}) ≼ (𝐶 ×
{1𝑜})) |
8 | | xp01disj 7576 |
. . . . 5
⊢ ((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) = ∅ |
9 | | undom 8048 |
. . . . 5
⊢ ((((𝐴 × {∅}) ≼
(𝐵 × {∅}) ∧
(𝐶 ×
{1𝑜}) ≼ (𝐶 × {1𝑜})) ∧
((𝐵 × {∅})
∩ (𝐶 ×
{1𝑜})) = ∅) → ((𝐴 × {∅}) ∪ (𝐶 × {1𝑜})) ≼
((𝐵 × {∅})
∪ (𝐶 ×
{1𝑜}))) |
10 | 8, 9 | mpan2 707 |
. . . 4
⊢ (((𝐴 × {∅}) ≼
(𝐵 × {∅}) ∧
(𝐶 ×
{1𝑜}) ≼ (𝐶 × {1𝑜})) →
((𝐴 × {∅})
∪ (𝐶 ×
{1𝑜})) ≼ ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
11 | 2, 7, 10 | syl2an 494 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → ((𝐴 × {∅}) ∪ (𝐶 × {1𝑜})) ≼
((𝐵 × {∅})
∪ (𝐶 ×
{1𝑜}))) |
12 | | reldom 7961 |
. . . . 5
⊢ Rel
≼ |
13 | 12 | brrelexi 5158 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
14 | | cdaval 8992 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 +𝑐 𝐶) = ((𝐴 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
15 | 13, 14 | sylan 488 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → (𝐴 +𝑐 𝐶) = ((𝐴 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
16 | 12 | brrelex2i 5159 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
17 | | cdaval 8992 |
. . . 4
⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
18 | 16, 17 | sylan 488 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
19 | 11, 15, 18 | 3brtr4d 4685 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ V) → (𝐴 +𝑐 𝐶) ≼ (𝐵 +𝑐 𝐶)) |
20 | | simpr 477 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → ¬ 𝐶 ∈ V) |
21 | 20 | intnand 962 |
. . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → ¬ (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
22 | | cdafn 8991 |
. . . . . 6
⊢
+𝑐 Fn (V × V) |
23 | | fndm 5990 |
. . . . . 6
⊢ (
+𝑐 Fn (V × V) → dom +𝑐 = (V
× V)) |
24 | 22, 23 | ax-mp 5 |
. . . . 5
⊢ dom
+𝑐 = (V × V) |
25 | 24 | ndmov 6818 |
. . . 4
⊢ (¬
(𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 +𝑐 𝐶) = ∅) |
26 | 21, 25 | syl 17 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 +𝑐 𝐶) = ∅) |
27 | | ovex 6678 |
. . . 4
⊢ (𝐵 +𝑐 𝐶) ∈ V |
28 | 27 | 0dom 8090 |
. . 3
⊢ ∅
≼ (𝐵
+𝑐 𝐶) |
29 | 26, 28 | syl6eqbr 4692 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐶 ∈ V) → (𝐴 +𝑐 𝐶) ≼ (𝐵 +𝑐 𝐶)) |
30 | 19, 29 | pm2.61dan 832 |
1
⊢ (𝐴 ≼ 𝐵 → (𝐴 +𝑐 𝐶) ≼ (𝐵 +𝑐 𝐶)) |