Proof of Theorem infdju
Step | Hyp | Ref
| Expression |
1 | | unnum 9952 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card) |
2 | 1 | 3adant3 1131 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 ∪ 𝐵) ∈ dom card) |
3 | | ssun2 4107 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
4 | | ssdomg 8786 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∈ dom card → (𝐵 ⊆ (𝐴 ∪ 𝐵) → 𝐵 ≼ (𝐴 ∪ 𝐵))) |
5 | 2, 3, 4 | mpisyl 21 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → 𝐵 ≼ (𝐴 ∪ 𝐵)) |
6 | | simp1 1135 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → 𝐴 ∈ dom
card) |
7 | | djudom2 9939 |
. . . . 5
⊢ ((𝐵 ≼ (𝐴 ∪ 𝐵) ∧ 𝐴 ∈ dom card) → (𝐴 ⊔ 𝐵) ≼ (𝐴 ⊔ (𝐴 ∪ 𝐵))) |
8 | 5, 6, 7 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 ⊔ 𝐵) ≼ (𝐴 ⊔ (𝐴 ∪ 𝐵))) |
9 | | djucomen 9933 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ (𝐴 ∪ 𝐵) ∈ dom card) → (𝐴 ⊔ (𝐴 ∪ 𝐵)) ≈ ((𝐴 ∪ 𝐵) ⊔ 𝐴)) |
10 | 6, 2, 9 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 ⊔ (𝐴 ∪ 𝐵)) ≈ ((𝐴 ∪ 𝐵) ⊔ 𝐴)) |
11 | | domentr 8799 |
. . . 4
⊢ (((𝐴 ⊔ 𝐵) ≼ (𝐴 ⊔ (𝐴 ∪ 𝐵)) ∧ (𝐴 ⊔ (𝐴 ∪ 𝐵)) ≈ ((𝐴 ∪ 𝐵) ⊔ 𝐴)) → (𝐴 ⊔ 𝐵) ≼ ((𝐴 ∪ 𝐵) ⊔ 𝐴)) |
12 | 8, 10, 11 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 ⊔ 𝐵) ≼ ((𝐴 ∪ 𝐵) ⊔ 𝐴)) |
13 | | simp3 1137 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → ω
≼ 𝐴) |
14 | | ssun1 4106 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
15 | | ssdomg 8786 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∈ dom card → (𝐴 ⊆ (𝐴 ∪ 𝐵) → 𝐴 ≼ (𝐴 ∪ 𝐵))) |
16 | 2, 14, 15 | mpisyl 21 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → 𝐴 ≼ (𝐴 ∪ 𝐵)) |
17 | | domtr 8793 |
. . . . 5
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ (𝐴 ∪ 𝐵)) → ω ≼ (𝐴 ∪ 𝐵)) |
18 | 13, 16, 17 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → ω
≼ (𝐴 ∪ 𝐵)) |
19 | | infdjuabs 9962 |
. . . 4
⊢ (((𝐴 ∪ 𝐵) ∈ dom card ∧ ω ≼
(𝐴 ∪ 𝐵) ∧ 𝐴 ≼ (𝐴 ∪ 𝐵)) → ((𝐴 ∪ 𝐵) ⊔ 𝐴) ≈ (𝐴 ∪ 𝐵)) |
20 | 2, 18, 16, 19 | syl3anc 1370 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → ((𝐴 ∪ 𝐵) ⊔ 𝐴) ≈ (𝐴 ∪ 𝐵)) |
21 | | domentr 8799 |
. . 3
⊢ (((𝐴 ⊔ 𝐵) ≼ ((𝐴 ∪ 𝐵) ⊔ 𝐴) ∧ ((𝐴 ∪ 𝐵) ⊔ 𝐴) ≈ (𝐴 ∪ 𝐵)) → (𝐴 ⊔ 𝐵) ≼ (𝐴 ∪ 𝐵)) |
22 | 12, 20, 21 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 ⊔ 𝐵) ≼ (𝐴 ∪ 𝐵)) |
23 | | undjudom 9923 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ≼ (𝐴 ⊔ 𝐵)) |
24 | 23 | 3adant3 1131 |
. 2
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 ⊔ 𝐵)) |
25 | | sbth 8880 |
. 2
⊢ (((𝐴 ⊔ 𝐵) ≼ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ≼ (𝐴 ⊔ 𝐵)) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵)) |
26 | 22, 24, 25 | syl2anc 584 |
1
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵)) |