Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → 𝐴 ≼ 𝐵) |
2 | | domsdomtr 9063 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≺ ω) → 𝐴 ≺ ω) |
3 | 1, 2 | sylan 581 |
. . . 4
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ 𝐵 ≺ ω) → 𝐴 ≺ ω) |
4 | | unfi2 9266 |
. . . 4
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω) |
5 | 3, 4 | sylancom 589 |
. . 3
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω) |
6 | | simpllr 775 |
. . 3
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ 𝐵 ≺ ω) → ω ≼
𝑋) |
7 | | sdomdomtr 9061 |
. . 3
⊢ (((𝐴 ∪ 𝐵) ≺ ω ∧ ω ≼
𝑋) → (𝐴 ∪ 𝐵) ≺ 𝑋) |
8 | 5, 6, 7 | syl2anc 585 |
. 2
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ 𝑋) |
9 | | omelon 9589 |
. . . . . 6
⊢ ω
∈ On |
10 | | onenon 9892 |
. . . . . 6
⊢ (ω
∈ On → ω ∈ dom card) |
11 | 9, 10 | ax-mp 5 |
. . . . 5
⊢ ω
∈ dom card |
12 | | simpll 766 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → 𝑋 ∈ dom card) |
13 | | sdomdom 8927 |
. . . . . . 7
⊢ (𝐵 ≺ 𝑋 → 𝐵 ≼ 𝑋) |
14 | 13 | ad2antll 728 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → 𝐵 ≼ 𝑋) |
15 | | numdom 9981 |
. . . . . 6
⊢ ((𝑋 ∈ dom card ∧ 𝐵 ≼ 𝑋) → 𝐵 ∈ dom card) |
16 | 12, 14, 15 | syl2anc 585 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → 𝐵 ∈ dom card) |
17 | | domtri2 9932 |
. . . . 5
⊢ ((ω
∈ dom card ∧ 𝐵
∈ dom card) → (ω ≼ 𝐵 ↔ ¬ 𝐵 ≺ ω)) |
18 | 11, 16, 17 | sylancr 588 |
. . . 4
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → (ω ≼ 𝐵 ↔ ¬ 𝐵 ≺ ω)) |
19 | 18 | biimpar 479 |
. . 3
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ¬ 𝐵 ≺ ω) → ω ≼
𝐵) |
20 | | uncom 4118 |
. . . . 5
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) |
21 | 16 | adantr 482 |
. . . . . 6
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ω ≼ 𝐵) → 𝐵 ∈ dom card) |
22 | | simpr 486 |
. . . . . 6
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ω ≼ 𝐵) → ω ≼ 𝐵) |
23 | 1 | adantr 482 |
. . . . . 6
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ω ≼ 𝐵) → 𝐴 ≼ 𝐵) |
24 | | infunabs 10150 |
. . . . . 6
⊢ ((𝐵 ∈ dom card ∧ ω
≼ 𝐵 ∧ 𝐴 ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) |
25 | 21, 22, 23, 24 | syl3anc 1372 |
. . . . 5
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ω ≼ 𝐵) → (𝐵 ∪ 𝐴) ≈ 𝐵) |
26 | 20, 25 | eqbrtrid 5145 |
. . . 4
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ω ≼ 𝐵) → (𝐴 ∪ 𝐵) ≈ 𝐵) |
27 | | simplrr 777 |
. . . 4
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ω ≼ 𝐵) → 𝐵 ≺ 𝑋) |
28 | | ensdomtr 9064 |
. . . 4
⊢ (((𝐴 ∪ 𝐵) ≈ 𝐵 ∧ 𝐵 ≺ 𝑋) → (𝐴 ∪ 𝐵) ≺ 𝑋) |
29 | 26, 27, 28 | syl2anc 585 |
. . 3
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ω ≼ 𝐵) → (𝐴 ∪ 𝐵) ≺ 𝑋) |
30 | 19, 29 | syldan 592 |
. 2
⊢ ((((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) ∧ ¬ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ 𝑋) |
31 | 8, 30 | pm2.61dan 812 |
1
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → (𝐴 ∪ 𝐵) ≺ 𝑋) |