Proof of Theorem infdif
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ∈ dom card) |
2 | | difss 3737 |
. . 3
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 |
3 | | ssdomg 8001 |
. . 3
⊢ (𝐴 ∈ dom card → ((𝐴 ∖ 𝐵) ⊆ 𝐴 → (𝐴 ∖ 𝐵) ≼ 𝐴)) |
4 | 1, 2, 3 | mpisyl 21 |
. 2
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≼ 𝐴) |
5 | | sdomdom 7983 |
. . . . . . . . 9
⊢ (𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴) |
6 | 5 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ≼ 𝐴) |
7 | | numdom 8861 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) |
8 | 1, 6, 7 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ∈ dom card) |
9 | | unnum 9022 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card) |
10 | 1, 8, 9 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∪ 𝐵) ∈ dom card) |
11 | | ssun1 3776 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
12 | | ssdomg 8001 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∈ dom card → (𝐴 ⊆ (𝐴 ∪ 𝐵) → 𝐴 ≼ (𝐴 ∪ 𝐵))) |
13 | 10, 11, 12 | mpisyl 21 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ (𝐴 ∪ 𝐵)) |
14 | | undif1 4043 |
. . . . . 6
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
15 | | ssnum 8862 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝐴 ∖ 𝐵) ∈ dom card) |
16 | 1, 2, 15 | sylancl 694 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ∈ dom card) |
17 | | uncdadom 8993 |
. . . . . . 7
⊢ (((𝐴 ∖ 𝐵) ∈ dom card ∧ 𝐵 ∈ dom card) → ((𝐴 ∖ 𝐵) ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵)) |
18 | 16, 8, 17 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵)) |
19 | 14, 18 | syl5eqbrr 4689 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵)) |
20 | | domtr 8009 |
. . . . 5
⊢ ((𝐴 ≼ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵)) → 𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵)) |
21 | 13, 19, 20 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵)) |
22 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ≺ 𝐴) |
23 | | sdomdom 7983 |
. . . . . . . . 9
⊢ ((𝐴 ∖ 𝐵) ≺ 𝐵 → (𝐴 ∖ 𝐵) ≼ 𝐵) |
24 | | cdadom1 9008 |
. . . . . . . . 9
⊢ ((𝐴 ∖ 𝐵) ≼ 𝐵 → ((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵)) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∖ 𝐵) ≺ 𝐵 → ((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵)) |
26 | | domtr 8009 |
. . . . . . . . . . 11
⊢ ((𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵) ∧ ((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵)) → 𝐴 ≼ (𝐵 +𝑐 𝐵)) |
27 | 26 | ex 450 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵) → (((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵) → 𝐴 ≼ (𝐵 +𝑐 𝐵))) |
28 | 21, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵) → 𝐴 ≼ (𝐵 +𝑐 𝐵))) |
29 | | simp2 1062 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ω ≼ 𝐴) |
30 | | domtr 8009 |
. . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ (𝐵 +𝑐 𝐵)) → ω ≼ (𝐵 +𝑐 𝐵)) |
31 | 30 | ex 450 |
. . . . . . . . . . . 12
⊢ (ω
≼ 𝐴 → (𝐴 ≼ (𝐵 +𝑐 𝐵) → ω ≼ (𝐵 +𝑐 𝐵))) |
32 | 29, 31 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ≼ (𝐵 +𝑐 𝐵) → ω ≼ (𝐵 +𝑐 𝐵))) |
33 | | cdainf 9014 |
. . . . . . . . . . . . 13
⊢ (ω
≼ 𝐵 ↔ ω
≼ (𝐵
+𝑐 𝐵)) |
34 | 33 | biimpri 218 |
. . . . . . . . . . . 12
⊢ (ω
≼ (𝐵
+𝑐 𝐵)
→ ω ≼ 𝐵) |
35 | | domrefg 7990 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom card → 𝐵 ≼ 𝐵) |
36 | | infcdaabs 9028 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ dom card ∧ ω
≼ 𝐵 ∧ 𝐵 ≼ 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵) |
37 | 36 | 3com23 1271 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ dom card ∧ 𝐵 ≼ 𝐵 ∧ ω ≼ 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵) |
38 | 37 | 3expia 1267 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ dom card ∧ 𝐵 ≼ 𝐵) → (ω ≼ 𝐵 → (𝐵 +𝑐 𝐵) ≈ 𝐵)) |
39 | 35, 38 | mpdan 702 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ dom card → (ω
≼ 𝐵 → (𝐵 +𝑐 𝐵) ≈ 𝐵)) |
40 | 8, 34, 39 | syl2im 40 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (ω ≼ (𝐵 +𝑐 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵)) |
41 | 32, 40 | syld 47 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ≼ (𝐵 +𝑐 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵)) |
42 | | domen2 8103 |
. . . . . . . . . . 11
⊢ ((𝐵 +𝑐 𝐵) ≈ 𝐵 → (𝐴 ≼ (𝐵 +𝑐 𝐵) ↔ 𝐴 ≼ 𝐵)) |
43 | 42 | biimpcd 239 |
. . . . . . . . . 10
⊢ (𝐴 ≼ (𝐵 +𝑐 𝐵) → ((𝐵 +𝑐 𝐵) ≈ 𝐵 → 𝐴 ≼ 𝐵)) |
44 | 41, 43 | sylcom 30 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ≼ (𝐵 +𝑐 𝐵) → 𝐴 ≼ 𝐵)) |
45 | 28, 44 | syld 47 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵) → 𝐴 ≼ 𝐵)) |
46 | | domnsym 8086 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴) |
47 | 25, 45, 46 | syl56 36 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴)) |
48 | 22, 47 | mt2d 131 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ¬ (𝐴 ∖ 𝐵) ≺ 𝐵) |
49 | | domtri2 8815 |
. . . . . . 7
⊢ ((𝐵 ∈ dom card ∧ (𝐴 ∖ 𝐵) ∈ dom card) → (𝐵 ≼ (𝐴 ∖ 𝐵) ↔ ¬ (𝐴 ∖ 𝐵) ≺ 𝐵)) |
50 | 8, 16, 49 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐵 ≼ (𝐴 ∖ 𝐵) ↔ ¬ (𝐴 ∖ 𝐵) ≺ 𝐵)) |
51 | 48, 50 | mpbird 247 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ≼ (𝐴 ∖ 𝐵)) |
52 | | cdadom2 9009 |
. . . . 5
⊢ (𝐵 ≼ (𝐴 ∖ 𝐵) → ((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) |
53 | 51, 52 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) |
54 | | domtr 8009 |
. . . 4
⊢ ((𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 𝐵) ∧ ((𝐴 ∖ 𝐵) +𝑐 𝐵) ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) → 𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) |
55 | 21, 53, 54 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) |
56 | | domtr 8009 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) → ω ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) |
57 | 29, 55, 56 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ω ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) |
58 | | cdainf 9014 |
. . . . 5
⊢ (ω
≼ (𝐴 ∖ 𝐵) ↔ ω ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵))) |
59 | 57, 58 | sylibr 224 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ω ≼ (𝐴 ∖ 𝐵)) |
60 | | domrefg 7990 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∈ dom card → (𝐴 ∖ 𝐵) ≼ (𝐴 ∖ 𝐵)) |
61 | 16, 60 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≼ (𝐴 ∖ 𝐵)) |
62 | | infcdaabs 9028 |
. . . 4
⊢ (((𝐴 ∖ 𝐵) ∈ dom card ∧ ω ≼
(𝐴 ∖ 𝐵) ∧ (𝐴 ∖ 𝐵) ≼ (𝐴 ∖ 𝐵)) → ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵)) ≈ (𝐴 ∖ 𝐵)) |
63 | 16, 59, 61, 62 | syl3anc 1326 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵)) ≈ (𝐴 ∖ 𝐵)) |
64 | | domentr 8015 |
. . 3
⊢ ((𝐴 ≼ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵)) ∧ ((𝐴 ∖ 𝐵) +𝑐 (𝐴 ∖ 𝐵)) ≈ (𝐴 ∖ 𝐵)) → 𝐴 ≼ (𝐴 ∖ 𝐵)) |
65 | 55, 63, 64 | syl2anc 693 |
. 2
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ (𝐴 ∖ 𝐵)) |
66 | | sbth 8080 |
. 2
⊢ (((𝐴 ∖ 𝐵) ≼ 𝐴 ∧ 𝐴 ≼ (𝐴 ∖ 𝐵)) → (𝐴 ∖ 𝐵) ≈ 𝐴) |
67 | 4, 65, 66 | syl2anc 693 |
1
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≈ 𝐴) |