Proof of Theorem omcan
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | omordi 8605 | . . . . . . . . 9
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶))) | 
| 2 | 1 | ex 412 | . . . . . . . 8
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (∅
∈ 𝐴 → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))) | 
| 3 | 2 | ancoms 458 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐴 → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))) | 
| 4 | 3 | 3adant2 1131 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐴 → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))) | 
| 5 | 4 | imp 406 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶))) | 
| 6 |  | omordi 8605 | . . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵))) | 
| 7 | 6 | ex 412 | . . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → (∅
∈ 𝐴 → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 8 | 7 | ancoms 458 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐴 → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 9 | 8 | 3adant3 1132 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐴 → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 10 | 9 | imp 406 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵))) | 
| 11 | 5, 10 | orim12d 966 | . . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵) → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 12 | 11 | con3d 152 | . . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)) → ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | 
| 13 |  | omcl 8575 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) | 
| 14 |  | eloni 6393 | . . . . . . 7
⊢ ((𝐴 ·o 𝐵) ∈ On → Ord (𝐴 ·o 𝐵)) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord (𝐴 ·o 𝐵)) | 
| 16 |  | omcl 8575 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐶) ∈ On) | 
| 17 |  | eloni 6393 | . . . . . . 7
⊢ ((𝐴 ·o 𝐶) ∈ On → Ord (𝐴 ·o 𝐶)) | 
| 18 | 16, 17 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → Ord (𝐴 ·o 𝐶)) | 
| 19 |  | ordtri3 6419 | . . . . . 6
⊢ ((Ord
(𝐴 ·o
𝐵) ∧ Ord (𝐴 ·o 𝐶)) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 20 | 15, 18, 19 | syl2an 596 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ∈ On ∧ 𝐶 ∈ On)) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 21 | 20 | 3impdi 1350 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 22 | 21 | adantr 480 | . . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) | 
| 23 |  | eloni 6393 | . . . . . 6
⊢ (𝐵 ∈ On → Ord 𝐵) | 
| 24 |  | eloni 6393 | . . . . . 6
⊢ (𝐶 ∈ On → Ord 𝐶) | 
| 25 |  | ordtri3 6419 | . . . . . 6
⊢ ((Ord
𝐵 ∧ Ord 𝐶) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | 
| 26 | 23, 24, 25 | syl2an 596 | . . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | 
| 27 | 26 | 3adant1 1130 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | 
| 28 | 27 | adantr 480 | . . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) | 
| 29 | 12, 22, 28 | 3imtr4d 294 | . 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶)) | 
| 30 |  | oveq2 7440 | . 2
⊢ (𝐵 = 𝐶 → (𝐴 ·o 𝐵) = (𝐴 ·o 𝐶)) | 
| 31 | 29, 30 | impbid1 225 | 1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ 𝐵 = 𝐶)) |