Proof of Theorem oeordsuc
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | onelon 6409 | . . . 4
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) | 
| 2 | 1 | ex 412 | . . 3
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → 𝐴 ∈ On)) | 
| 3 | 2 | adantr 480 | . 2
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → 𝐴 ∈ On)) | 
| 4 |  | oewordri 8630 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶))) | 
| 5 | 4 | 3adant1 1131 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶))) | 
| 6 |  | oecl 8575 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On) | 
| 7 | 6 | 3adant2 1132 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On) | 
| 8 |  | oecl 8575 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑o 𝐶) ∈ On) | 
| 9 | 8 | 3adant1 1131 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑o 𝐶) ∈ On) | 
| 10 |  | simp1 1137 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐴 ∈ On) | 
| 11 |  | omwordri 8610 | . . . . . . . . . . 11
⊢ (((𝐴 ↑o 𝐶) ∈ On ∧ (𝐵 ↑o 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶) → ((𝐴 ↑o 𝐶) ·o 𝐴) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴))) | 
| 12 | 7, 9, 10, 11 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐶) ⊆ (𝐵 ↑o 𝐶) → ((𝐴 ↑o 𝐶) ·o 𝐴) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴))) | 
| 13 | 5, 12 | syld 47 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐴 ↑o 𝐶) ·o 𝐴) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴))) | 
| 14 |  | oesuc 8565 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o suc 𝐶) = ((𝐴 ↑o 𝐶) ·o 𝐴)) | 
| 15 | 14 | 3adant2 1132 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o suc 𝐶) = ((𝐴 ↑o 𝐶) ·o 𝐴)) | 
| 16 | 15 | sseq1d 4015 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴) ↔ ((𝐴 ↑o 𝐶) ·o 𝐴) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴))) | 
| 17 | 13, 16 | sylibrd 259 | . . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴))) | 
| 18 |  | ne0i 4341 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) | 
| 19 |  | on0eln0 6440 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) | 
| 20 | 18, 19 | imbitrrid 246 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → ∅ ∈ 𝐵)) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ∅ ∈ 𝐵)) | 
| 22 |  | oen0 8624 | . . . . . . . . . . . . 13
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐵) → ∅ ∈
(𝐵 ↑o 𝐶)) | 
| 23 | 22 | ex 412 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐵 → ∅
∈ (𝐵
↑o 𝐶))) | 
| 24 | 21, 23 | syld 47 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ∅ ∈ (𝐵 ↑o 𝐶))) | 
| 25 |  | omordi 8604 | . . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ On ∧ (𝐵 ↑o 𝐶) ∈ On) ∧ ∅
∈ (𝐵
↑o 𝐶))
→ (𝐴 ∈ 𝐵 → ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ ((𝐵 ↑o 𝐶) ·o 𝐵))) | 
| 26 | 8, 25 | syldanl 602 | . . . . . . . . . . . . 13
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
(𝐵 ↑o 𝐶)) → (𝐴 ∈ 𝐵 → ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ ((𝐵 ↑o 𝐶) ·o 𝐵))) | 
| 27 | 26 | ex 412 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
↑o 𝐶)
→ (𝐴 ∈ 𝐵 → ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ ((𝐵 ↑o 𝐶) ·o 𝐵)))) | 
| 28 | 27 | com23 86 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (∅ ∈ (𝐵 ↑o 𝐶) → ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ ((𝐵 ↑o 𝐶) ·o 𝐵)))) | 
| 29 | 24, 28 | mpdd 43 | . . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ ((𝐵 ↑o 𝐶) ·o 𝐵))) | 
| 30 | 29 | 3adant1 1131 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ ((𝐵 ↑o 𝐶) ·o 𝐵))) | 
| 31 |  | oesuc 8565 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑o suc 𝐶) = ((𝐵 ↑o 𝐶) ·o 𝐵)) | 
| 32 | 31 | 3adant1 1131 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ↑o suc 𝐶) = ((𝐵 ↑o 𝐶) ·o 𝐵)) | 
| 33 | 32 | eleq2d 2827 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶) ↔ ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ ((𝐵 ↑o 𝐶) ·o 𝐵))) | 
| 34 | 30, 33 | sylibrd 259 | . . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶))) | 
| 35 | 17, 34 | jcad 512 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴) ∧ ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶)))) | 
| 36 | 35 | 3expa 1119 | . . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → ((𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴) ∧ ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶)))) | 
| 37 |  | onsucb 7837 | . . . . . . 7
⊢ (𝐶 ∈ On ↔ suc 𝐶 ∈ On) | 
| 38 |  | oecl 8575 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴 ↑o suc 𝐶) ∈ On) | 
| 39 |  | oecl 8575 | . . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ suc 𝐶 ∈ On) → (𝐵 ↑o suc 𝐶) ∈ On) | 
| 40 |  | ontr2 6431 | . . . . . . . . 9
⊢ (((𝐴 ↑o suc 𝐶) ∈ On ∧ (𝐵 ↑o suc 𝐶) ∈ On) → (((𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴) ∧ ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶)) → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))) | 
| 41 | 38, 39, 40 | syl2an 596 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ suc 𝐶 ∈ On) ∧ (𝐵 ∈ On ∧ suc 𝐶 ∈ On)) → (((𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴) ∧ ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶)) → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))) | 
| 42 | 41 | anandirs 679 | . . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ suc 𝐶 ∈ On) → (((𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴) ∧ ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶)) → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))) | 
| 43 | 37, 42 | sylan2b 594 | . . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑o suc 𝐶) ⊆ ((𝐵 ↑o 𝐶) ·o 𝐴) ∧ ((𝐵 ↑o 𝐶) ·o 𝐴) ∈ (𝐵 ↑o suc 𝐶)) → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))) | 
| 44 | 36, 43 | syld 47 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))) | 
| 45 | 44 | exp31 419 | . . . 4
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ∈ 𝐵 → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))))) | 
| 46 | 45 | com4l 92 | . . 3
⊢ (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ∈ 𝐵 → (𝐴 ∈ On → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))))) | 
| 47 | 46 | imp 406 | . 2
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ∈ On → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶)))) | 
| 48 | 3, 47 | mpdd 43 | 1
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 ↑o suc 𝐶) ∈ (𝐵 ↑o suc 𝐶))) |