Proof of Theorem oewordi
| Step | Hyp | Ref
| Expression |
| 1 | | eloni 6394 |
. . . . . 6
⊢ (𝐶 ∈ On → Ord 𝐶) |
| 2 | | ordgt0ge1 8531 |
. . . . . 6
⊢ (Ord
𝐶 → (∅ ∈
𝐶 ↔ 1o
⊆ 𝐶)) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔
1o ⊆ 𝐶)) |
| 4 | | 1on 8518 |
. . . . . 6
⊢
1o ∈ On |
| 5 | | onsseleq 6425 |
. . . . . 6
⊢
((1o ∈ On ∧ 𝐶 ∈ On) → (1o ⊆
𝐶 ↔ (1o
∈ 𝐶 ∨ 1o
= 𝐶))) |
| 6 | 4, 5 | mpan 690 |
. . . . 5
⊢ (𝐶 ∈ On → (1o
⊆ 𝐶 ↔
(1o ∈ 𝐶
∨ 1o = 𝐶))) |
| 7 | 3, 6 | bitrd 279 |
. . . 4
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔
(1o ∈ 𝐶
∨ 1o = 𝐶))) |
| 8 | 7 | 3ad2ant3 1136 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 ↔
(1o ∈ 𝐶
∨ 1o = 𝐶))) |
| 9 | | ondif2 8540 |
. . . . . . 7
⊢ (𝐶 ∈ (On ∖
2o) ↔ (𝐶
∈ On ∧ 1o ∈ 𝐶)) |
| 10 | | oeword 8628 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴
⊆ 𝐵 ↔ (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵))) |
| 11 | 10 | biimpd 229 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴
⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵))) |
| 12 | 11 | 3expia 1122 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ (On ∖
2o) → (𝐴
⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵)))) |
| 13 | 9, 12 | biimtrrid 243 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 1o
∈ 𝐶) → (𝐴 ⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵)))) |
| 14 | 13 | expd 415 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ On → (1o
∈ 𝐶 → (𝐴 ⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵))))) |
| 15 | 14 | 3impia 1118 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
(1o ∈ 𝐶
→ (𝐴 ⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵)))) |
| 16 | | oe1m 8583 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (1o
↑o 𝐴) =
1o) |
| 17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1o ↑o 𝐴) = 1o) |
| 18 | | oe1m 8583 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → (1o
↑o 𝐵) =
1o) |
| 19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1o ↑o 𝐵) = 1o) |
| 20 | 17, 19 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1o ↑o 𝐴) = (1o ↑o 𝐵)) |
| 21 | | eqimss 4042 |
. . . . . . . 8
⊢
((1o ↑o 𝐴) = (1o ↑o 𝐵) → (1o
↑o 𝐴)
⊆ (1o ↑o 𝐵)) |
| 22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1o ↑o 𝐴) ⊆ (1o ↑o
𝐵)) |
| 23 | | oveq1 7438 |
. . . . . . . 8
⊢
(1o = 𝐶
→ (1o ↑o 𝐴) = (𝐶 ↑o 𝐴)) |
| 24 | | oveq1 7438 |
. . . . . . . 8
⊢
(1o = 𝐶
→ (1o ↑o 𝐵) = (𝐶 ↑o 𝐵)) |
| 25 | 23, 24 | sseq12d 4017 |
. . . . . . 7
⊢
(1o = 𝐶
→ ((1o ↑o 𝐴) ⊆ (1o ↑o
𝐵) ↔ (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵))) |
| 26 | 22, 25 | syl5ibcom 245 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1o = 𝐶 →
(𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵))) |
| 27 | 26 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
(1o = 𝐶 →
(𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵))) |
| 28 | 27 | a1dd 50 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
(1o = 𝐶 →
(𝐴 ⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵)))) |
| 29 | 15, 28 | jaod 860 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) →
((1o ∈ 𝐶
∨ 1o = 𝐶)
→ (𝐴 ⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵)))) |
| 30 | 8, 29 | sylbid 240 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 → (𝐴 ⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵)))) |
| 31 | 30 | imp 406 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ⊆ 𝐵 → (𝐶 ↑o 𝐴) ⊆ (𝐶 ↑o 𝐵))) |