Proof of Theorem oeordsuc
Step | Hyp | Ref
| Expression |
1 | | onelon 5748 |
. . . 4
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
2 | 1 | ex 450 |
. . 3
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → 𝐴 ∈ On)) |
3 | 2 | adantr 481 |
. 2
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → 𝐴 ∈ On)) |
4 | | oewordri 7672 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑𝑜 𝐶) ⊆ (𝐵 ↑𝑜 𝐶))) |
5 | 4 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑𝑜 𝐶) ⊆ (𝐵 ↑𝑜 𝐶))) |
6 | | oecl 7617 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜
𝐶) ∈
On) |
7 | 6 | 3adant2 1080 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜
𝐶) ∈
On) |
8 | | oecl 7617 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑𝑜
𝐶) ∈
On) |
9 | 8 | 3adant1 1079 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑𝑜
𝐶) ∈
On) |
10 | | simp1 1061 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐴 ∈ On) |
11 | | omwordri 7652 |
. . . . . . . . . . 11
⊢ (((𝐴 ↑𝑜
𝐶) ∈ On ∧ (𝐵 ↑𝑜
𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ↑𝑜
𝐶) ⊆ (𝐵 ↑𝑜
𝐶) → ((𝐴 ↑𝑜
𝐶)
·𝑜 𝐴) ⊆ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴))) |
12 | 7, 9, 10, 11 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜
𝐶) ⊆ (𝐵 ↑𝑜
𝐶) → ((𝐴 ↑𝑜
𝐶)
·𝑜 𝐴) ⊆ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴))) |
13 | 5, 12 | syld 47 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐴 ↑𝑜 𝐶) ·𝑜
𝐴) ⊆ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴))) |
14 | | oesuc 7607 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜 suc
𝐶) = ((𝐴 ↑𝑜 𝐶) ·𝑜
𝐴)) |
15 | 14 | 3adant2 1080 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜 suc
𝐶) = ((𝐴 ↑𝑜 𝐶) ·𝑜
𝐴)) |
16 | 15 | sseq1d 3632 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜 suc
𝐶) ⊆ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ↔ ((𝐴 ↑𝑜 𝐶) ·𝑜
𝐴) ⊆ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴))) |
17 | 13, 16 | sylibrd 249 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑𝑜 suc 𝐶) ⊆ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴))) |
18 | | ne0i 3921 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) |
19 | | on0eln0 5780 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
20 | 18, 19 | syl5ibr 236 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → ∅ ∈ 𝐵)) |
21 | 20 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ∅ ∈ 𝐵)) |
22 | | oen0 7666 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐵) → ∅ ∈
(𝐵
↑𝑜 𝐶)) |
23 | 22 | ex 450 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐵 → ∅
∈ (𝐵
↑𝑜 𝐶))) |
24 | 21, 23 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ∅ ∈ (𝐵 ↑𝑜 𝐶))) |
25 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On) |
26 | 25, 8 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ On ∧ (𝐵 ↑𝑜
𝐶) ∈
On)) |
27 | | omordi 7646 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ On ∧ (𝐵 ↑𝑜
𝐶) ∈ On) ∧ ∅
∈ (𝐵
↑𝑜 𝐶)) → (𝐴 ∈ 𝐵 → ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐵))) |
28 | 26, 27 | sylan 488 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
(𝐵
↑𝑜 𝐶)) → (𝐴 ∈ 𝐵 → ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐵))) |
29 | 28 | ex 450 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
↑𝑜 𝐶) → (𝐴 ∈ 𝐵 → ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐵)))) |
30 | 29 | com23 86 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (∅ ∈ (𝐵 ↑𝑜 𝐶) → ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐵)))) |
31 | 24, 30 | mpdd 43 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐵))) |
32 | 31 | 3adant1 1079 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐵))) |
33 | | oesuc 7607 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑𝑜 suc
𝐶) = ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐵)) |
34 | 33 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑𝑜 suc
𝐶) = ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐵)) |
35 | 34 | eleq2d 2687 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ∈ (𝐵 ↑𝑜 suc 𝐶) ↔ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐵))) |
36 | 32, 35 | sylibrd 249 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ (𝐵 ↑𝑜 suc
𝐶))) |
37 | 17, 36 | jcad 555 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐴 ↑𝑜 suc 𝐶) ⊆ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∧ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ∈ (𝐵 ↑𝑜 suc 𝐶)))) |
38 | 37 | 3expa 1265 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐴 ↑𝑜 suc 𝐶) ⊆ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∧ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ∈ (𝐵 ↑𝑜 suc 𝐶)))) |
39 | | sucelon 7017 |
. . . . . . 7
⊢ (𝐶 ∈ On ↔ suc 𝐶 ∈ On) |
40 | | oecl 7617 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴 ↑𝑜 suc
𝐶) ∈
On) |
41 | | oecl 7617 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ suc 𝐶 ∈ On) → (𝐵 ↑𝑜 suc
𝐶) ∈
On) |
42 | | ontr2 5772 |
. . . . . . . . 9
⊢ (((𝐴 ↑𝑜 suc
𝐶) ∈ On ∧ (𝐵 ↑𝑜 suc
𝐶) ∈ On) →
(((𝐴
↑𝑜 suc 𝐶) ⊆ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∧ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ∈ (𝐵 ↑𝑜 suc 𝐶)) → (𝐴 ↑𝑜 suc 𝐶) ∈ (𝐵 ↑𝑜 suc 𝐶))) |
43 | 40, 41, 42 | syl2an 494 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ suc 𝐶 ∈ On) ∧ (𝐵 ∈ On ∧ suc 𝐶 ∈ On)) → (((𝐴 ↑𝑜 suc
𝐶) ⊆ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ∧ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ (𝐵 ↑𝑜 suc
𝐶)) → (𝐴 ↑𝑜 suc
𝐶) ∈ (𝐵 ↑𝑜 suc
𝐶))) |
44 | 43 | anandirs 874 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc 𝐶 ∈ On) → (((𝐴 ↑𝑜 suc
𝐶) ⊆ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ∧ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ (𝐵 ↑𝑜 suc
𝐶)) → (𝐴 ↑𝑜 suc
𝐶) ∈ (𝐵 ↑𝑜 suc
𝐶))) |
45 | 39, 44 | sylan2b 492 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑𝑜 suc
𝐶) ⊆ ((𝐵 ↑𝑜
𝐶)
·𝑜 𝐴) ∧ ((𝐵 ↑𝑜 𝐶) ·𝑜
𝐴) ∈ (𝐵 ↑𝑜 suc
𝐶)) → (𝐴 ↑𝑜 suc
𝐶) ∈ (𝐵 ↑𝑜 suc
𝐶))) |
46 | 38, 45 | syld 47 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑𝑜 suc 𝐶) ∈ (𝐵 ↑𝑜 suc 𝐶))) |
47 | 46 | exp31 630 |
. . . 4
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ∈ 𝐵 → (𝐴 ↑𝑜 suc 𝐶) ∈ (𝐵 ↑𝑜 suc 𝐶))))) |
48 | 47 | com4l 92 |
. . 3
⊢ (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ∈ 𝐵 → (𝐴 ∈ On → (𝐴 ↑𝑜 suc 𝐶) ∈ (𝐵 ↑𝑜 suc 𝐶))))) |
49 | 48 | imp 445 |
. 2
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ∈ On → (𝐴 ↑𝑜 suc 𝐶) ∈ (𝐵 ↑𝑜 suc 𝐶)))) |
50 | 3, 49 | mpdd 43 |
1
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑𝑜 suc 𝐶) ∈ (𝐵 ↑𝑜 suc 𝐶))) |