Proof of Theorem infdif
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ∈ dom card) | 
| 2 |  | difss 4135 | . . 3
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 | 
| 3 |  | ssdomg 9041 | . . 3
⊢ (𝐴 ∈ dom card → ((𝐴 ∖ 𝐵) ⊆ 𝐴 → (𝐴 ∖ 𝐵) ≼ 𝐴)) | 
| 4 | 1, 2, 3 | mpisyl 21 | . 2
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≼ 𝐴) | 
| 5 |  | sdomdom 9021 | . . . . . . . . 9
⊢ (𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴) | 
| 6 | 5 | 3ad2ant3 1135 | . . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ≼ 𝐴) | 
| 7 |  | numdom 10079 | . . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | 
| 8 | 1, 6, 7 | syl2anc 584 | . . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ∈ dom card) | 
| 9 |  | unnum 10238 | . . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card) | 
| 10 | 1, 8, 9 | syl2anc 584 | . . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∪ 𝐵) ∈ dom card) | 
| 11 |  | ssun1 4177 | . . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | 
| 12 |  | ssdomg 9041 | . . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∈ dom card → (𝐴 ⊆ (𝐴 ∪ 𝐵) → 𝐴 ≼ (𝐴 ∪ 𝐵))) | 
| 13 | 10, 11, 12 | mpisyl 21 | . . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ (𝐴 ∪ 𝐵)) | 
| 14 |  | undif1 4475 | . . . . . 6
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) | 
| 15 |  | ssnum 10080 | . . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝐴 ∖ 𝐵) ∈ dom card) | 
| 16 | 1, 2, 15 | sylancl 586 | . . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ∈ dom card) | 
| 17 |  | undjudom 10209 | . . . . . . 7
⊢ (((𝐴 ∖ 𝐵) ∈ dom card ∧ 𝐵 ∈ dom card) → ((𝐴 ∖ 𝐵) ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵)) | 
| 18 | 16, 8, 17 | syl2anc 584 | . . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵)) | 
| 19 | 14, 18 | eqbrtrrid 5178 | . . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵)) | 
| 20 |  | domtr 9048 | . . . . 5
⊢ ((𝐴 ≼ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵)) → 𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵)) | 
| 21 | 13, 19, 20 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵)) | 
| 22 |  | simp3 1138 | . . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ≺ 𝐴) | 
| 23 |  | sdomdom 9021 | . . . . . . . . 9
⊢ ((𝐴 ∖ 𝐵) ≺ 𝐵 → (𝐴 ∖ 𝐵) ≼ 𝐵) | 
| 24 |  | relsdom 8993 | . . . . . . . . . 10
⊢ Rel
≺ | 
| 25 | 24 | brrelex2i 5741 | . . . . . . . . 9
⊢ ((𝐴 ∖ 𝐵) ≺ 𝐵 → 𝐵 ∈ V) | 
| 26 |  | djudom1 10224 | . . . . . . . . 9
⊢ (((𝐴 ∖ 𝐵) ≼ 𝐵 ∧ 𝐵 ∈ V) → ((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ (𝐵 ⊔ 𝐵)) | 
| 27 | 23, 25, 26 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∖ 𝐵) ≺ 𝐵 → ((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ (𝐵 ⊔ 𝐵)) | 
| 28 |  | domtr 9048 | . . . . . . . . . . 11
⊢ ((𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵) ∧ ((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ (𝐵 ⊔ 𝐵)) → 𝐴 ≼ (𝐵 ⊔ 𝐵)) | 
| 29 | 28 | ex 412 | . . . . . . . . . 10
⊢ (𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵) → (((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ (𝐵 ⊔ 𝐵) → 𝐴 ≼ (𝐵 ⊔ 𝐵))) | 
| 30 | 21, 29 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ (𝐵 ⊔ 𝐵) → 𝐴 ≼ (𝐵 ⊔ 𝐵))) | 
| 31 |  | simp2 1137 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ω ≼ 𝐴) | 
| 32 |  | domtr 9048 | . . . . . . . . . . . . 13
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ (𝐵 ⊔ 𝐵)) → ω ≼ (𝐵 ⊔ 𝐵)) | 
| 33 | 32 | ex 412 | . . . . . . . . . . . 12
⊢ (ω
≼ 𝐴 → (𝐴 ≼ (𝐵 ⊔ 𝐵) → ω ≼ (𝐵 ⊔ 𝐵))) | 
| 34 | 31, 33 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ≼ (𝐵 ⊔ 𝐵) → ω ≼ (𝐵 ⊔ 𝐵))) | 
| 35 |  | djuinf 10230 | . . . . . . . . . . . . 13
⊢ (ω
≼ 𝐵 ↔ ω
≼ (𝐵 ⊔ 𝐵)) | 
| 36 | 35 | biimpri 228 | . . . . . . . . . . . 12
⊢ (ω
≼ (𝐵 ⊔ 𝐵) → ω ≼ 𝐵) | 
| 37 |  | domrefg 9028 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom card → 𝐵 ≼ 𝐵) | 
| 38 |  | infdjuabs 10246 | . . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ dom card ∧ ω
≼ 𝐵 ∧ 𝐵 ≼ 𝐵) → (𝐵 ⊔ 𝐵) ≈ 𝐵) | 
| 39 | 38 | 3com23 1126 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ dom card ∧ 𝐵 ≼ 𝐵 ∧ ω ≼ 𝐵) → (𝐵 ⊔ 𝐵) ≈ 𝐵) | 
| 40 | 39 | 3expia 1121 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ dom card ∧ 𝐵 ≼ 𝐵) → (ω ≼ 𝐵 → (𝐵 ⊔ 𝐵) ≈ 𝐵)) | 
| 41 | 37, 40 | mpdan 687 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ dom card → (ω
≼ 𝐵 → (𝐵 ⊔ 𝐵) ≈ 𝐵)) | 
| 42 | 8, 36, 41 | syl2im 40 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (ω ≼ (𝐵 ⊔ 𝐵) → (𝐵 ⊔ 𝐵) ≈ 𝐵)) | 
| 43 | 34, 42 | syld 47 | . . . . . . . . . 10
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ≼ (𝐵 ⊔ 𝐵) → (𝐵 ⊔ 𝐵) ≈ 𝐵)) | 
| 44 |  | domen2 9161 | . . . . . . . . . . 11
⊢ ((𝐵 ⊔ 𝐵) ≈ 𝐵 → (𝐴 ≼ (𝐵 ⊔ 𝐵) ↔ 𝐴 ≼ 𝐵)) | 
| 45 | 44 | biimpcd 249 | . . . . . . . . . 10
⊢ (𝐴 ≼ (𝐵 ⊔ 𝐵) → ((𝐵 ⊔ 𝐵) ≈ 𝐵 → 𝐴 ≼ 𝐵)) | 
| 46 | 43, 45 | sylcom 30 | . . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ≼ (𝐵 ⊔ 𝐵) → 𝐴 ≼ 𝐵)) | 
| 47 | 30, 46 | syld 47 | . . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ (𝐵 ⊔ 𝐵) → 𝐴 ≼ 𝐵)) | 
| 48 |  | domnsym 9140 | . . . . . . . 8
⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴) | 
| 49 | 27, 47, 48 | syl56 36 | . . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴)) | 
| 50 | 22, 49 | mt2d 136 | . . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ¬ (𝐴 ∖ 𝐵) ≺ 𝐵) | 
| 51 |  | domtri2 10030 | . . . . . . 7
⊢ ((𝐵 ∈ dom card ∧ (𝐴 ∖ 𝐵) ∈ dom card) → (𝐵 ≼ (𝐴 ∖ 𝐵) ↔ ¬ (𝐴 ∖ 𝐵) ≺ 𝐵)) | 
| 52 | 8, 16, 51 | syl2anc 584 | . . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐵 ≼ (𝐴 ∖ 𝐵) ↔ ¬ (𝐴 ∖ 𝐵) ≺ 𝐵)) | 
| 53 | 50, 52 | mpbird 257 | . . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐵 ≼ (𝐴 ∖ 𝐵)) | 
| 54 | 1 | difexd 5330 | . . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ∈ V) | 
| 55 |  | djudom2 10225 | . . . . 5
⊢ ((𝐵 ≼ (𝐴 ∖ 𝐵) ∧ (𝐴 ∖ 𝐵) ∈ V) → ((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) | 
| 56 | 53, 54, 55 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) | 
| 57 |  | domtr 9048 | . . . 4
⊢ ((𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ 𝐵) ∧ ((𝐴 ∖ 𝐵) ⊔ 𝐵) ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) → 𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) | 
| 58 | 21, 56, 57 | syl2anc 584 | . . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) | 
| 59 |  | domtr 9048 | . . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) → ω ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) | 
| 60 | 31, 58, 59 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ω ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) | 
| 61 |  | djuinf 10230 | . . . . 5
⊢ (ω
≼ (𝐴 ∖ 𝐵) ↔ ω ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵))) | 
| 62 | 60, 61 | sylibr 234 | . . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ω ≼ (𝐴 ∖ 𝐵)) | 
| 63 |  | domrefg 9028 | . . . . 5
⊢ ((𝐴 ∖ 𝐵) ∈ dom card → (𝐴 ∖ 𝐵) ≼ (𝐴 ∖ 𝐵)) | 
| 64 | 16, 63 | syl 17 | . . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≼ (𝐴 ∖ 𝐵)) | 
| 65 |  | infdjuabs 10246 | . . . 4
⊢ (((𝐴 ∖ 𝐵) ∈ dom card ∧ ω ≼
(𝐴 ∖ 𝐵) ∧ (𝐴 ∖ 𝐵) ≼ (𝐴 ∖ 𝐵)) → ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵)) ≈ (𝐴 ∖ 𝐵)) | 
| 66 | 16, 62, 64, 65 | syl3anc 1372 | . . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵)) ≈ (𝐴 ∖ 𝐵)) | 
| 67 |  | domentr 9054 | . . 3
⊢ ((𝐴 ≼ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵)) ∧ ((𝐴 ∖ 𝐵) ⊔ (𝐴 ∖ 𝐵)) ≈ (𝐴 ∖ 𝐵)) → 𝐴 ≼ (𝐴 ∖ 𝐵)) | 
| 68 | 58, 66, 67 | syl2anc 584 | . 2
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → 𝐴 ≼ (𝐴 ∖ 𝐵)) | 
| 69 |  | sbth 9134 | . 2
⊢ (((𝐴 ∖ 𝐵) ≼ 𝐴 ∧ 𝐴 ≼ (𝐴 ∖ 𝐵)) → (𝐴 ∖ 𝐵) ≈ 𝐴) | 
| 70 | 4, 68, 69 | syl2anc 584 | 1
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≈ 𝐴) |