Proof of Theorem infxp
Step | Hyp | Ref
| Expression |
1 | | sdomdom 7983 |
. . 3
⊢ (𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴) |
2 | | infxpabs 9034 |
. . . . . 6
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ 𝐴) |
3 | | infunabs 9029 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) |
4 | 3 | 3expa 1265 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) |
5 | 4 | adantrl 752 |
. . . . . . 7
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 ∪ 𝐵) ≈ 𝐴) |
6 | 5 | ensymd 8007 |
. . . . . 6
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ (𝐴 ∪ 𝐵)) |
7 | | entr 8008 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≈ 𝐴 ∧ 𝐴 ≈ (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
8 | 2, 6, 7 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
9 | 8 | expr 643 |
. . . 4
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝐵 ≠ ∅) → (𝐵 ≼ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
10 | 9 | adantrl 752 |
. . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵 ≼ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
11 | 1, 10 | syl5 34 |
. 2
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵 ≺ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
12 | | domtri2 8815 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) |
13 | 12 | ad2ant2r 783 |
. . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) |
14 | | xpcomeng 8052 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
15 | 14 | ad2ant2r 783 |
. . . . . 6
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
16 | 15 | adantr 481 |
. . . . 5
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
17 | | simplrl 800 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐵 ∈ dom card) |
18 | | simplr 792 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → ω
≼ 𝐴) |
19 | | domtr 8009 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ 𝐵) → ω ≼ 𝐵) |
20 | 18, 19 | sylan 488 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → ω ≼ 𝐵) |
21 | | infn0 8222 |
. . . . . . . 8
⊢ (ω
≼ 𝐴 → 𝐴 ≠ ∅) |
22 | 21 | ad3antlr 767 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐴 ≠ ∅) |
23 | | simpr 477 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐵) |
24 | | infxpabs 9034 |
. . . . . . 7
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧ (𝐴 ≠ ∅ ∧ 𝐴 ≼ 𝐵)) → (𝐵 × 𝐴) ≈ 𝐵) |
25 | 17, 20, 22, 23, 24 | syl22anc 1327 |
. . . . . 6
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 × 𝐴) ≈ 𝐵) |
26 | | uncom 3757 |
. . . . . . . 8
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) |
27 | | infunabs 9029 |
. . . . . . . . 9
⊢ ((𝐵 ∈ dom card ∧ ω
≼ 𝐵 ∧ 𝐴 ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) |
28 | 17, 20, 23, 27 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) |
29 | 26, 28 | syl5eqbr 4688 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐴 ∪ 𝐵) ≈ 𝐵) |
30 | 29 | ensymd 8007 |
. . . . . 6
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐵 ≈ (𝐴 ∪ 𝐵)) |
31 | | entr 8008 |
. . . . . 6
⊢ (((𝐵 × 𝐴) ≈ 𝐵 ∧ 𝐵 ≈ (𝐴 ∪ 𝐵)) → (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) |
32 | 25, 30, 31 | syl2anc 693 |
. . . . 5
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) |
33 | | entr 8008 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≈ (𝐵 × 𝐴) ∧ (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
34 | 16, 32, 33 | syl2anc 693 |
. . . 4
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |
35 | 34 | ex 450 |
. . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 ≼ 𝐵 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
36 | 13, 35 | sylbird 250 |
. 2
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (¬
𝐵 ≺ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) |
37 | 11, 36 | pm2.61d 170 |
1
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |