Proof of Theorem gchdomtri
Step | Hyp | Ref
| Expression |
1 | | sdomdom 8223 |
. . . . 5
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) |
2 | 1 | con3i 152 |
. . . 4
⊢ (¬
𝐴 ≼ 𝐵 → ¬ 𝐴 ≺ 𝐵) |
3 | | reldom 8201 |
. . . . . . 7
⊢ Rel
≼ |
4 | 3 | brrelex1i 5363 |
. . . . . 6
⊢ (𝐵 ≼ 𝒫 𝐴 → 𝐵 ∈ V) |
5 | 4 | 3ad2ant3 1166 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ∈ V) |
6 | | fidomtri2 9106 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → (𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵)) |
7 | 5, 6 | sylan 576 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵)) |
8 | 2, 7 | syl5ibr 238 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (¬ 𝐴 ≼ 𝐵 → 𝐵 ≼ 𝐴)) |
9 | 8 | orrd 890 |
. 2
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
10 | | simp1 1167 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ∈ GCH) |
11 | 10 | adantr 473 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ GCH) |
12 | | simpr 478 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin) |
13 | | cdadom3 9298 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ 𝐵 ∈ V) → 𝐴 ≼ (𝐴 +𝑐 𝐵)) |
14 | 10, 5, 13 | syl2anc 580 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ≼ (𝐴 +𝑐 𝐵)) |
15 | 14 | adantr 473 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ (𝐴 +𝑐 𝐵)) |
16 | | cdalepw 9306 |
. . . . . 6
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
17 | 16 | 3adant1 1161 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
18 | 17 | adantr 473 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
19 | | gchor 9737 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ (𝐴 +𝑐 𝐵) ∧ (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴)) → (𝐴 ≈ (𝐴 +𝑐 𝐵) ∨ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴)) |
20 | 11, 12, 15, 18, 19 | syl22anc 868 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≈ (𝐴 +𝑐 𝐵) ∨ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴)) |
21 | | cdadom3 9298 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ GCH) → 𝐵 ≼ (𝐵 +𝑐 𝐴)) |
22 | 5, 10, 21 | syl2anc 580 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≼ (𝐵 +𝑐 𝐴)) |
23 | | cdacomen 9291 |
. . . . . . . 8
⊢ (𝐵 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵) |
24 | | domentr 8254 |
. . . . . . . 8
⊢ ((𝐵 ≼ (𝐵 +𝑐 𝐴) ∧ (𝐵 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵)) → 𝐵 ≼ (𝐴 +𝑐 𝐵)) |
25 | 22, 23, 24 | sylancl 581 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≼ (𝐴 +𝑐 𝐵)) |
26 | | domen2 8345 |
. . . . . . 7
⊢ (𝐴 ≈ (𝐴 +𝑐 𝐵) → (𝐵 ≼ 𝐴 ↔ 𝐵 ≼ (𝐴 +𝑐 𝐵))) |
27 | 25, 26 | syl5ibrcom 239 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≈ (𝐴 +𝑐 𝐵) → 𝐵 ≼ 𝐴)) |
28 | 27 | imp 396 |
. . . . 5
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≈ (𝐴 +𝑐 𝐵)) → 𝐵 ≼ 𝐴) |
29 | 28 | olcd 901 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≈ (𝐴 +𝑐 𝐵)) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
30 | | simpl1 1243 |
. . . . . . 7
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝐴 ∈ GCH) |
31 | | canth2g 8356 |
. . . . . . 7
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
32 | | sdomdom 8223 |
. . . . . . 7
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝐴 ≼ 𝒫 𝐴) |
34 | | simpl2 1245 |
. . . . . . . . 9
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → (𝐴 +𝑐 𝐴) ≈ 𝐴) |
35 | | pwen 8375 |
. . . . . . . . 9
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝐴 → 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴) |
37 | | enen2 8343 |
. . . . . . . . 9
⊢ ((𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴 → (𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵) ↔ 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)) |
38 | 37 | adantl 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → (𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵) ↔ 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)) |
39 | 36, 38 | mpbird 249 |
. . . . . . 7
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵)) |
40 | | endom 8222 |
. . . . . . 7
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≈ (𝐴
+𝑐 𝐵)
→ 𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)) |
41 | | pwcdadom 9326 |
. . . . . . 7
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ 𝒫 𝐴 ≼
𝐵) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝒫 𝐴 ≼ 𝐵) |
43 | | domtr 8248 |
. . . . . 6
⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐵) |
44 | 33, 42, 43 | syl2anc 580 |
. . . . 5
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝐴 ≼ 𝐵) |
45 | 44 | orcd 900 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
46 | 29, 45 | jaodan 981 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ≈ (𝐴 +𝑐 𝐵) ∨ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴)) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
47 | 20, 46 | syldan 586 |
. 2
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
48 | 9, 47 | pm2.61dan 848 |
1
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |