Proof of Theorem infxp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sdomdom 9021 | . . 3
⊢ (𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴) | 
| 2 |  | infxpabs 10252 | . . . . . 6
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ 𝐴) | 
| 3 |  | infunabs 10247 | . . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) | 
| 4 | 3 | 3expa 1118 | . . . . . . . 8
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) | 
| 5 | 4 | adantrl 716 | . . . . . . 7
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 ∪ 𝐵) ≈ 𝐴) | 
| 6 | 5 | ensymd 9046 | . . . . . 6
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ (𝐴 ∪ 𝐵)) | 
| 7 |  | entr 9047 | . . . . . 6
⊢ (((𝐴 × 𝐵) ≈ 𝐴 ∧ 𝐴 ≈ (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) | 
| 8 | 2, 6, 7 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) | 
| 9 | 8 | expr 456 | . . . 4
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝐵 ≠ ∅) → (𝐵 ≼ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) | 
| 10 | 9 | adantrl 716 | . . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵 ≼ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) | 
| 11 | 1, 10 | syl5 34 | . 2
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵 ≺ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) | 
| 12 |  | domtri2 10030 | . . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | 
| 13 | 12 | ad2ant2r 747 | . . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | 
| 14 |  | xpcomeng 9105 | . . . . . 6
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) | 
| 15 | 14 | ad2ant2r 747 | . . . . 5
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) | 
| 16 |  | simplrl 776 | . . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐵 ∈ dom card) | 
| 17 |  | domtr 9048 | . . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ 𝐵) → ω ≼ 𝐵) | 
| 18 | 17 | ad4ant24 754 | . . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → ω ≼ 𝐵) | 
| 19 |  | infn0 9341 | . . . . . . . 8
⊢ (ω
≼ 𝐴 → 𝐴 ≠ ∅) | 
| 20 | 19 | ad3antlr 731 | . . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐴 ≠ ∅) | 
| 21 |  | simpr 484 | . . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐵) | 
| 22 |  | infxpabs 10252 | . . . . . . 7
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧ (𝐴 ≠ ∅ ∧ 𝐴 ≼ 𝐵)) → (𝐵 × 𝐴) ≈ 𝐵) | 
| 23 | 16, 18, 20, 21, 22 | syl22anc 838 | . . . . . 6
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 × 𝐴) ≈ 𝐵) | 
| 24 |  | uncom 4157 | . . . . . . . 8
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | 
| 25 |  | infunabs 10247 | . . . . . . . . 9
⊢ ((𝐵 ∈ dom card ∧ ω
≼ 𝐵 ∧ 𝐴 ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) | 
| 26 | 16, 18, 21, 25 | syl3anc 1372 | . . . . . . . 8
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) | 
| 27 | 24, 26 | eqbrtrid 5177 | . . . . . . 7
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐴 ∪ 𝐵) ≈ 𝐵) | 
| 28 | 27 | ensymd 9046 | . . . . . 6
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → 𝐵 ≈ (𝐴 ∪ 𝐵)) | 
| 29 |  | entr 9047 | . . . . . 6
⊢ (((𝐵 × 𝐴) ≈ 𝐵 ∧ 𝐵 ≈ (𝐴 ∪ 𝐵)) → (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) | 
| 30 | 23, 28, 29 | syl2anc 584 | . . . . 5
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) | 
| 31 |  | entr 9047 | . . . . 5
⊢ (((𝐴 × 𝐵) ≈ (𝐵 × 𝐴) ∧ (𝐵 × 𝐴) ≈ (𝐴 ∪ 𝐵)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) | 
| 32 | 15, 30, 31 | syl2an2r 685 | . . . 4
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) | 
| 33 | 32 | ex 412 | . . 3
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 ≼ 𝐵 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) | 
| 34 | 13, 33 | sylbird 260 | . 2
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (¬
𝐵 ≺ 𝐴 → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))) | 
| 35 | 11, 34 | pm2.61d 179 | 1
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) |