Proof of Theorem gchdomtri
| Step | Hyp | Ref
| Expression |
| 1 | | sdomdom 9020 |
. . . . 5
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) |
| 2 | 1 | con3i 154 |
. . . 4
⊢ (¬
𝐴 ≼ 𝐵 → ¬ 𝐴 ≺ 𝐵) |
| 3 | | reldom 8991 |
. . . . . . 7
⊢ Rel
≼ |
| 4 | 3 | brrelex1i 5741 |
. . . . . 6
⊢ (𝐵 ≼ 𝒫 𝐴 → 𝐵 ∈ V) |
| 5 | 4 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ∈ V) |
| 6 | | fidomtri2 10034 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → (𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵)) |
| 7 | 5, 6 | sylan 580 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵)) |
| 8 | 2, 7 | imbitrrid 246 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (¬ 𝐴 ≼ 𝐵 → 𝐵 ≼ 𝐴)) |
| 9 | 8 | orrd 864 |
. 2
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
| 10 | | simp1 1137 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ∈ GCH) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ GCH) |
| 12 | | simpr 484 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin) |
| 13 | | djudoml 10225 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ 𝐵 ∈ V) → 𝐴 ≼ (𝐴 ⊔ 𝐵)) |
| 14 | 10, 5, 13 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ≼ (𝐴 ⊔ 𝐵)) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ (𝐴 ⊔ 𝐵)) |
| 16 | | djulepw 10233 |
. . . . . 6
⊢ (((𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ⊔ 𝐵) ≼ 𝒫 𝐴) |
| 17 | 16 | 3adant1 1131 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ⊔ 𝐵) ≼ 𝒫 𝐴) |
| 18 | 17 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐵) ≼ 𝒫 𝐴) |
| 19 | | gchor 10667 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ (𝐴 ⊔ 𝐵) ∧ (𝐴 ⊔ 𝐵) ≼ 𝒫 𝐴)) → (𝐴 ≈ (𝐴 ⊔ 𝐵) ∨ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴)) |
| 20 | 11, 12, 15, 18, 19 | syl22anc 839 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≈ (𝐴 ⊔ 𝐵) ∨ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴)) |
| 21 | | djudoml 10225 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ GCH) → 𝐵 ≼ (𝐵 ⊔ 𝐴)) |
| 22 | 5, 10, 21 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≼ (𝐵 ⊔ 𝐴)) |
| 23 | | djucomen 10218 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ GCH) → (𝐵 ⊔ 𝐴) ≈ (𝐴 ⊔ 𝐵)) |
| 24 | 5, 10, 23 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐵 ⊔ 𝐴) ≈ (𝐴 ⊔ 𝐵)) |
| 25 | | domentr 9053 |
. . . . . . . 8
⊢ ((𝐵 ≼ (𝐵 ⊔ 𝐴) ∧ (𝐵 ⊔ 𝐴) ≈ (𝐴 ⊔ 𝐵)) → 𝐵 ≼ (𝐴 ⊔ 𝐵)) |
| 26 | 22, 24, 25 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≼ (𝐴 ⊔ 𝐵)) |
| 27 | | domen2 9160 |
. . . . . . 7
⊢ (𝐴 ≈ (𝐴 ⊔ 𝐵) → (𝐵 ≼ 𝐴 ↔ 𝐵 ≼ (𝐴 ⊔ 𝐵))) |
| 28 | 26, 27 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≈ (𝐴 ⊔ 𝐵) → 𝐵 ≼ 𝐴)) |
| 29 | 28 | imp 406 |
. . . . 5
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≈ (𝐴 ⊔ 𝐵)) → 𝐵 ≼ 𝐴) |
| 30 | 29 | olcd 875 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≈ (𝐴 ⊔ 𝐵)) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
| 31 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → 𝐴 ∈ GCH) |
| 32 | | canth2g 9171 |
. . . . . . 7
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
| 33 | | sdomdom 9020 |
. . . . . . 7
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
| 34 | 31, 32, 33 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → 𝐴 ≼ 𝒫 𝐴) |
| 35 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → (𝐴 ⊔ 𝐴) ≈ 𝐴) |
| 36 | | pwen 9190 |
. . . . . . . . 9
⊢ ((𝐴 ⊔ 𝐴) ≈ 𝐴 → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
| 37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴) |
| 38 | | enen2 9158 |
. . . . . . . . 9
⊢ ((𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴 → (𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ 𝐵) ↔ 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)) |
| 39 | 38 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → (𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ 𝐵) ↔ 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)) |
| 40 | 37, 39 | mpbird 257 |
. . . . . . 7
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ 𝐵)) |
| 41 | | endom 9019 |
. . . . . . 7
⊢
(𝒫 (𝐴
⊔ 𝐴) ≈ (𝐴 ⊔ 𝐵) → 𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵)) |
| 42 | | pwdjudom 10255 |
. . . . . . 7
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵) |
| 43 | 40, 41, 42 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → 𝒫 𝐴 ≼ 𝐵) |
| 44 | | domtr 9047 |
. . . . . 6
⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐵) |
| 45 | 34, 43, 44 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → 𝐴 ≼ 𝐵) |
| 46 | 45 | orcd 874 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
| 47 | 30, 46 | jaodan 960 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ≈ (𝐴 ⊔ 𝐵) ∨ (𝐴 ⊔ 𝐵) ≈ 𝒫 𝐴)) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
| 48 | 20, 47 | syldan 591 |
. 2
⊢ (((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
| 49 | 9, 48 | pm2.61dan 813 |
1
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |