Proof of Theorem oneo
Step | Hyp | Ref
| Expression |
1 | | onnbtwn 5735 |
. . 3
⊢ (𝐴 ∈ On → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) |
2 | 1 | 3ad2ant1 1075 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) |
3 | | suceq 5707 |
. . . . 5
⊢ (𝐶 = (2𝑜
·𝑜 𝐴) → suc 𝐶 = suc (2𝑜
·𝑜 𝐴)) |
4 | 3 | eqeq1d 2612 |
. . . 4
⊢ (𝐶 = (2𝑜
·𝑜 𝐴) → (suc 𝐶 = (2𝑜
·𝑜 𝐵) ↔ suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵))) |
5 | 4 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → (suc 𝐶 = (2𝑜
·𝑜 𝐵) ↔ suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵))) |
6 | | ovex 6577 |
. . . . . . . 8
⊢
(2𝑜 ·𝑜 𝐴) ∈ V |
7 | 6 | sucid 5721 |
. . . . . . 7
⊢
(2𝑜 ·𝑜 𝐴) ∈ suc (2𝑜
·𝑜 𝐴) |
8 | | eleq2 2677 |
. . . . . . 7
⊢ (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → ((2𝑜
·𝑜 𝐴) ∈ suc (2𝑜
·𝑜 𝐴) ↔ (2𝑜
·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵))) |
9 | 7, 8 | mpbii 222 |
. . . . . 6
⊢ (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → (2𝑜
·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵)) |
10 | | 2on 7455 |
. . . . . . . 8
⊢
2𝑜 ∈ On |
11 | | omord 7535 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧
2𝑜 ∈ On) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵))) |
12 | 10, 11 | mp3an3 1405 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵))) |
13 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 2𝑜)
→ 𝐴 ∈ 𝐵) |
14 | 12, 13 | syl6bir 243 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
((2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵) → 𝐴 ∈ 𝐵)) |
15 | 9, 14 | syl5 33 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → 𝐴 ∈ 𝐵)) |
16 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) |
17 | | omcl 7503 |
. . . . . . . . . . . . 13
⊢
((2𝑜 ∈ On ∧ 𝐴 ∈ On) → (2𝑜
·𝑜 𝐴) ∈ On) |
18 | 10, 17 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On →
(2𝑜 ·𝑜 𝐴) ∈ On) |
19 | | oa1suc 7498 |
. . . . . . . . . . . 12
⊢
((2𝑜 ·𝑜 𝐴) ∈ On → ((2𝑜
·𝑜 𝐴) +𝑜
1𝑜) = suc (2𝑜
·𝑜 𝐴)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) = suc (2𝑜
·𝑜 𝐴)) |
21 | | 1on 7454 |
. . . . . . . . . . . . . . . 16
⊢
1𝑜 ∈ On |
22 | 21 | elexi 3186 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ∈ V |
23 | 22 | sucid 5721 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ suc 1𝑜 |
24 | | df-2o 7448 |
. . . . . . . . . . . . . 14
⊢
2𝑜 = suc 1𝑜 |
25 | 23, 24 | eleqtrri 2687 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ 2𝑜 |
26 | | oaord 7514 |
. . . . . . . . . . . . . . 15
⊢
((1𝑜 ∈ On ∧ 2𝑜 ∈ On
∧ (2𝑜 ·𝑜 𝐴) ∈ On) → (1𝑜
∈ 2𝑜 ↔ ((2𝑜
·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜))) |
27 | 21, 10, 26 | mp3an12 1406 |
. . . . . . . . . . . . . 14
⊢
((2𝑜 ·𝑜 𝐴) ∈ On → (1𝑜
∈ 2𝑜 ↔ ((2𝑜
·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜))) |
28 | 18, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On →
(1𝑜 ∈ 2𝑜 ↔
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜))) |
29 | 25, 28 | mpbii 222 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On →
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜)) |
30 | | omsuc 7493 |
. . . . . . . . . . . . 13
⊢
((2𝑜 ∈ On ∧ 𝐴 ∈ On) → (2𝑜
·𝑜 suc 𝐴) = ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜)) |
31 | 10, 30 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On →
(2𝑜 ·𝑜 suc 𝐴) = ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜)) |
32 | 29, 31 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ (2𝑜
·𝑜 suc 𝐴)) |
33 | 20, 32 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → suc
(2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 suc 𝐴)) |
34 | 33 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → suc (2𝑜
·𝑜 𝐴) ∈ (2𝑜
·𝑜 suc 𝐴)) |
35 | 16, 34 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → (2𝑜
·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴)) |
36 | | suceloni 6905 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
37 | | omord 7535 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ suc 𝐴 ∈ On ∧
2𝑜 ∈ On) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
38 | 10, 37 | mp3an3 1405 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ suc 𝐴 ∈ On) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
39 | 36, 38 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
40 | 39 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
41 | 40 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
42 | 35, 41 | mpbird 246 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → (𝐵 ∈ suc 𝐴 ∧ ∅ ∈
2𝑜)) |
43 | 42 | simpld 474 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → 𝐵 ∈ suc 𝐴) |
44 | 43 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → 𝐵 ∈ suc 𝐴)) |
45 | 15, 44 | jcad 554 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))) |
46 | 45 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → (suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))) |
47 | 5, 46 | sylbid 229 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → (suc 𝐶 = (2𝑜
·𝑜 𝐵) → (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))) |
48 | 2, 47 | mtod 188 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → ¬ suc 𝐶 = (2𝑜
·𝑜 𝐵)) |