Step | Hyp | Ref
| Expression |
1 | | sdomdom 8975 |
. . 3
⊢ (𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴) |
2 | | infxpabs 10206 |
. . . . . 6
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ 𝐴) |
3 | | infunabs 10201 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) |
4 | 3 | 3expa 1118 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) |
5 | 4 | adantrl 714 |
. . . . . . 7
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 ∪ 𝐵) ≈ 𝐴) |
6 | 5 | ensymd 9000 |
. . . . . 6
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ (𝐴 ∪ 𝐵)) |
7 | | entr 9001 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≈ 𝐴 ∧ 𝐴 ≈ (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
8 | 2, 6, 7 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
9 | 8 | expr 457 |
. . . 4
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝐵 ≠ ∅) → (𝐵 ≼ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
10 | 9 | adantrl 714 |
. . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵 ≼ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
11 | 1, 10 | syl5 34 |
. 2
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵 ≺ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
12 | | domtri2 9983 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) |
13 | 12 | ad2ant2r 745 |
. . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) |
14 | | xpcomeng 9063 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
15 | 14 | ad2ant2r 745 |
. . . . 5
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
16 | | simplrl 775 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐵 ∈ dom card) |
17 | | domtr 9002 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ 𝐵) → ω ≼ 𝐵) |
18 | 17 | ad4ant24 752 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → ω ≼ 𝐵) |
19 | | infn0 9306 |
. . . . . . . 8
⊢ (ω
≼ 𝐴 → 𝐴 ≠ ∅) |
20 | 19 | ad3antlr 729 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐴 ≠ ∅) |
21 | | simpr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐵) |
22 | | infxpabs 10206 |
. . . . . . 7
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧ (𝐴 ≠ ∅ ∧ 𝐴 ≼ 𝐵)) → (𝐵 × 𝐴) ≈ 𝐵) |
23 | 16, 18, 20, 21, 22 | syl22anc 837 |
. . . . . 6
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 × 𝐴) ≈ 𝐵) |
24 | | uncom 4153 |
. . . . . . . 8
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) |
25 | | infunabs 10201 |
. . . . . . . . 9
⊢ ((𝐵 ∈ dom card ∧ ω
≼ 𝐵 ∧ 𝐴 ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) |
26 | 16, 18, 21, 25 | syl3anc 1371 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) |
27 | 24, 26 | eqbrtrid 5183 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐴 ∪ 𝐵) ≈ 𝐵) |
28 | 27 | ensymd 9000 |
. . . . . 6
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐵 ≈ (𝐴 ∪ 𝐵)) |
29 | | entr 9001 |
. . . . . 6
⊢ (((𝐵 × 𝐴) ≈ 𝐵 ∧ 𝐵 ≈ (𝐴 ∪ 𝐵)) → (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) |
30 | 23, 28, 29 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) |
31 | | entr 9001 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≈ (𝐵 × 𝐴) ∧ (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
32 | 15, 30, 31 | syl2an2r 683 |
. . . 4
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
33 | 32 | ex 413 |
. . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 ≼ 𝐵 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
34 | 13, 33 | sylbird 259 |
. 2
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (¬
𝐵 ≺ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
35 | 11, 34 | pm2.61d 179 |
1
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |