Proof of Theorem oewordi
Step | Hyp | Ref
| Expression |
1 | | eloni 5733 |
. . . . . 6
⊢ (𝐶 ∈ On → Ord 𝐶) |
2 | | ordgt0ge1 7577 |
. . . . . 6
⊢ (Ord
𝐶 → (∅ ∈
𝐶 ↔
1𝑜 ⊆ 𝐶)) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔
1𝑜 ⊆ 𝐶)) |
4 | | 1on 7567 |
. . . . . 6
⊢
1𝑜 ∈ On |
5 | | onsseleq 5765 |
. . . . . 6
⊢
((1𝑜 ∈ On ∧ 𝐶 ∈ On) → (1𝑜
⊆ 𝐶 ↔
(1𝑜 ∈ 𝐶 ∨ 1𝑜 = 𝐶))) |
6 | 4, 5 | mpan 706 |
. . . . 5
⊢ (𝐶 ∈ On →
(1𝑜 ⊆ 𝐶 ↔ (1𝑜 ∈ 𝐶 ∨ 1𝑜 =
𝐶))) |
7 | 3, 6 | bitrd 268 |
. . . 4
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔
(1𝑜 ∈ 𝐶 ∨ 1𝑜 = 𝐶))) |
8 | 7 | 3ad2ant3 1084 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 ↔
(1𝑜 ∈ 𝐶 ∨ 1𝑜 = 𝐶))) |
9 | | ondif2 7582 |
. . . . . . 7
⊢ (𝐶 ∈ (On ∖
2𝑜) ↔ (𝐶 ∈ On ∧ 1𝑜
∈ 𝐶)) |
10 | | oeword 7670 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵))) |
11 | 10 | biimpd 219 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵))) |
12 | 11 | 3expia 1267 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ (On ∖
2𝑜) → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵)))) |
13 | 9, 12 | syl5bir 233 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧
1𝑜 ∈ 𝐶) → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵)))) |
14 | 13 | expd 452 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ On →
(1𝑜 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵))))) |
15 | 14 | 3impia 1261 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
(1𝑜 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵)))) |
16 | | oe1m 7625 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
(1𝑜 ↑𝑜 𝐴) = 1𝑜) |
17 | 16 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1𝑜 ↑𝑜 𝐴) = 1𝑜) |
18 | | oe1m 7625 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On →
(1𝑜 ↑𝑜 𝐵) = 1𝑜) |
19 | 18 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1𝑜 ↑𝑜 𝐵) = 1𝑜) |
20 | 17, 19 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1𝑜 ↑𝑜 𝐴) = (1𝑜
↑𝑜 𝐵)) |
21 | | eqimss 3657 |
. . . . . . . 8
⊢
((1𝑜 ↑𝑜 𝐴) = (1𝑜
↑𝑜 𝐵) → (1𝑜
↑𝑜 𝐴) ⊆ (1𝑜
↑𝑜 𝐵)) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1𝑜 ↑𝑜 𝐴) ⊆ (1𝑜
↑𝑜 𝐵)) |
23 | | oveq1 6657 |
. . . . . . . 8
⊢
(1𝑜 = 𝐶 → (1𝑜
↑𝑜 𝐴) = (𝐶 ↑𝑜 𝐴)) |
24 | | oveq1 6657 |
. . . . . . . 8
⊢
(1𝑜 = 𝐶 → (1𝑜
↑𝑜 𝐵) = (𝐶 ↑𝑜 𝐵)) |
25 | 23, 24 | sseq12d 3634 |
. . . . . . 7
⊢
(1𝑜 = 𝐶 → ((1𝑜
↑𝑜 𝐴) ⊆ (1𝑜
↑𝑜 𝐵) ↔ (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵))) |
26 | 22, 25 | syl5ibcom 235 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1𝑜 = 𝐶
→ (𝐶
↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵))) |
27 | 26 | 3adant3 1081 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
(1𝑜 = 𝐶
→ (𝐶
↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵))) |
28 | 27 | a1dd 50 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
(1𝑜 = 𝐶
→ (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵)))) |
29 | 15, 28 | jaod 395 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
((1𝑜 ∈ 𝐶 ∨ 1𝑜 = 𝐶) → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵)))) |
30 | 8, 29 | sylbid 230 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵)))) |
31 | 30 | imp 445 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ⊆ 𝐵 → (𝐶 ↑𝑜 𝐴) ⊆ (𝐶 ↑𝑜 𝐵))) |