Step |
Hyp |
Ref |
Expression |
1 |
|
sdomdom |
⊢ ( 𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴 ) |
2 |
|
infxpabs |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ 𝐴 ) |
3 |
|
infunabs |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 ) |
4 |
3
|
3expa |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 ) |
5 |
4
|
adantrl |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 ) |
6 |
5
|
ensymd |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → 𝐴 ≈ ( 𝐴 ∪ 𝐵 ) ) |
7 |
|
entr |
⊢ ( ( ( 𝐴 × 𝐵 ) ≈ 𝐴 ∧ 𝐴 ≈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) |
8 |
2 6 7
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) |
9 |
8
|
expr |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝐵 ≠ ∅ ) → ( 𝐵 ≼ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) ) |
10 |
9
|
adantrl |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐵 ≼ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) ) |
11 |
1 10
|
syl5 |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐵 ≺ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) ) |
12 |
|
domtri2 |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) ) |
13 |
12
|
ad2ant2r |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) ) |
14 |
|
xpcomeng |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) ) |
15 |
14
|
ad2ant2r |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) ) |
16 |
|
simplrl |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐵 ∈ dom card ) |
17 |
|
domtr |
⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → ω ≼ 𝐵 ) |
18 |
17
|
ad4ant24 |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ω ≼ 𝐵 ) |
19 |
|
infn0 |
⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ ) |
20 |
19
|
ad3antlr |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≠ ∅ ) |
21 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≼ 𝐵 ) |
22 |
|
infxpabs |
⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ 𝐵 ) ) → ( 𝐵 × 𝐴 ) ≈ 𝐵 ) |
23 |
16 18 20 21 22
|
syl22anc |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 × 𝐴 ) ≈ 𝐵 ) |
24 |
|
uncom |
⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐴 ) |
25 |
|
infunabs |
⊢ ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 ∪ 𝐴 ) ≈ 𝐵 ) |
26 |
16 18 21 25
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 ∪ 𝐴 ) ≈ 𝐵 ) |
27 |
24 26
|
eqbrtrid |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐵 ) |
28 |
27
|
ensymd |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐵 ≈ ( 𝐴 ∪ 𝐵 ) ) |
29 |
|
entr |
⊢ ( ( ( 𝐵 × 𝐴 ) ≈ 𝐵 ∧ 𝐵 ≈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) ) |
30 |
23 28 29
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) ) |
31 |
|
entr |
⊢ ( ( ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) ∧ ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) |
32 |
15 30 31
|
syl2an2r |
⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) |
33 |
32
|
ex |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 ≼ 𝐵 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) ) |
34 |
13 33
|
sylbird |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( ¬ 𝐵 ≺ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) ) |
35 |
11 34
|
pm2.61d |
⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) |