Proof of Theorem gchdomtri
Step | Hyp | Ref
| Expression |
1 | | sdomdom 7983 |
. . . . 5
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) |
2 | 1 | con3i 150 |
. . . 4
⊢ (¬
𝐴 ≼ 𝐵 → ¬ 𝐴 ≺ 𝐵) |
3 | | reldom 7961 |
. . . . . . 7
⊢ Rel
≼ |
4 | 3 | brrelexi 5158 |
. . . . . 6
⊢ (𝐵 ≼ 𝒫 𝐴 → 𝐵 ∈ V) |
5 | 4 | 3ad2ant3 1084 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ∈ V) |
6 | | fidomtri2 8820 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → (𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵)) |
7 | 5, 6 | sylan 488 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵)) |
8 | 2, 7 | syl5ibr 236 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (¬ 𝐴 ≼ 𝐵 → 𝐵 ≼ 𝐴)) |
9 | 8 | orrd 393 |
. 2
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
10 | | simp1 1061 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ∈ GCH) |
11 | 10 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ GCH) |
12 | | simpr 477 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin) |
13 | | cdadom3 9010 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ 𝐵 ∈ V) → 𝐴 ≼ (𝐴 +𝑐 𝐵)) |
14 | 10, 5, 13 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ≼ (𝐴 +𝑐 𝐵)) |
15 | 14 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ≼ (𝐴 +𝑐 𝐵)) |
16 | | cdalepw 9018 |
. . . . . 6
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
17 | 16 | 3adant1 1079 |
. . . . 5
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
18 | 17 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
19 | | gchor 9449 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ (𝐴 +𝑐 𝐵) ∧ (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴)) → (𝐴 ≈ (𝐴 +𝑐 𝐵) ∨ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴)) |
20 | 11, 12, 15, 18, 19 | syl22anc 1327 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≈ (𝐴 +𝑐 𝐵) ∨ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴)) |
21 | | cdadom3 9010 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ GCH) → 𝐵 ≼ (𝐵 +𝑐 𝐴)) |
22 | 5, 10, 21 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≼ (𝐵 +𝑐 𝐴)) |
23 | | cdacomen 9003 |
. . . . . . . 8
⊢ (𝐵 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵) |
24 | | domentr 8015 |
. . . . . . . 8
⊢ ((𝐵 ≼ (𝐵 +𝑐 𝐴) ∧ (𝐵 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵)) → 𝐵 ≼ (𝐴 +𝑐 𝐵)) |
25 | 22, 23, 24 | sylancl 694 |
. . . . . . 7
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≼ (𝐴 +𝑐 𝐵)) |
26 | | domen2 8103 |
. . . . . . 7
⊢ (𝐴 ≈ (𝐴 +𝑐 𝐵) → (𝐵 ≼ 𝐴 ↔ 𝐵 ≼ (𝐴 +𝑐 𝐵))) |
27 | 25, 26 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≈ (𝐴 +𝑐 𝐵) → 𝐵 ≼ 𝐴)) |
28 | 27 | imp 445 |
. . . . 5
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≈ (𝐴 +𝑐 𝐵)) → 𝐵 ≼ 𝐴) |
29 | 28 | olcd 408 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≈ (𝐴 +𝑐 𝐵)) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
30 | | simpl1 1064 |
. . . . . . 7
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝐴 ∈ GCH) |
31 | | canth2g 8114 |
. . . . . . 7
⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴) |
32 | | sdomdom 7983 |
. . . . . . 7
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝐴 ≼ 𝒫 𝐴) |
34 | | simpl2 1065 |
. . . . . . . . 9
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → (𝐴 +𝑐 𝐴) ≈ 𝐴) |
35 | | pwen 8133 |
. . . . . . . . 9
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝐴 → 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴) |
37 | | enen2 8101 |
. . . . . . . . 9
⊢ ((𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴 → (𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵) ↔ 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)) |
38 | 37 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → (𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵) ↔ 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)) |
39 | 36, 38 | mpbird 247 |
. . . . . . 7
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 𝐵)) |
40 | | endom 7982 |
. . . . . . 7
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≈ (𝐴
+𝑐 𝐵)
→ 𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)) |
41 | | pwcdadom 9038 |
. . . . . . 7
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ 𝒫 𝐴 ≼
𝐵) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝒫 𝐴 ≼ 𝐵) |
43 | | domtr 8009 |
. . . . . 6
⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐵) |
44 | 33, 42, 43 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → 𝐴 ≼ 𝐵) |
45 | 44 | orcd 407 |
. . . 4
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
46 | 29, 45 | jaodan 826 |
. . 3
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ (𝐴 ≈ (𝐴 +𝑐 𝐵) ∨ (𝐴 +𝑐 𝐵) ≈ 𝒫 𝐴)) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
47 | 20, 46 | syldan 487 |
. 2
⊢ (((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |
48 | 9, 47 | pm2.61dan 832 |
1
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) |