Proof of Theorem omcan
Step | Hyp | Ref
| Expression |
1 | | omordi 8223 |
. . . . . . . . 9
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶))) |
2 | 1 | ex 416 |
. . . . . . . 8
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (∅
∈ 𝐴 → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))) |
3 | 2 | ancoms 462 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐴 → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))) |
4 | 3 | 3adant2 1132 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐴 → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))) |
5 | 4 | imp 410 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶))) |
6 | | omordi 8223 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵))) |
7 | 6 | ex 416 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → (∅
∈ 𝐴 → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
8 | 7 | ancoms 462 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐴 → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
9 | 8 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐴 → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
10 | 9 | imp 410 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (𝐶 ∈ 𝐵 → (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵))) |
11 | 5, 10 | orim12d 964 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵) → ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
12 | 11 | con3d 155 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)) → ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
13 | | omcl 8192 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
14 | | eloni 6182 |
. . . . . . 7
⊢ ((𝐴 ·o 𝐵) ∈ On → Ord (𝐴 ·o 𝐵)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord (𝐴 ·o 𝐵)) |
16 | | omcl 8192 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐶) ∈ On) |
17 | | eloni 6182 |
. . . . . . 7
⊢ ((𝐴 ·o 𝐶) ∈ On → Ord (𝐴 ·o 𝐶)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → Ord (𝐴 ·o 𝐶)) |
19 | | ordtri3 6208 |
. . . . . 6
⊢ ((Ord
(𝐴 ·o
𝐵) ∧ Ord (𝐴 ·o 𝐶)) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
20 | 15, 18, 19 | syl2an 599 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ∈ On ∧ 𝐶 ∈ On)) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
21 | 20 | 3impdi 1351 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
22 | 21 | adantr 484 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ ¬ ((𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶) ∨ (𝐴 ·o 𝐶) ∈ (𝐴 ·o 𝐵)))) |
23 | | eloni 6182 |
. . . . . 6
⊢ (𝐵 ∈ On → Ord 𝐵) |
24 | | eloni 6182 |
. . . . . 6
⊢ (𝐶 ∈ On → Ord 𝐶) |
25 | | ordtri3 6208 |
. . . . . 6
⊢ ((Ord
𝐵 ∧ Ord 𝐶) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
26 | 23, 24, 25 | syl2an 599 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
27 | 26 | 3adant1 1131 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
28 | 27 | adantr 484 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
29 | 12, 22, 28 | 3imtr4d 297 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶)) |
30 | | oveq2 7178 |
. 2
⊢ (𝐵 = 𝐶 → (𝐴 ·o 𝐵) = (𝐴 ·o 𝐶)) |
31 | 29, 30 | impbid1 228 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ 𝐵 = 𝐶)) |