Proof of Theorem om00
Step | Hyp | Ref
| Expression |
1 | | neanior 2886 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ ¬
(𝐴 = ∅ ∨ 𝐵 = ∅)) |
2 | | eloni 5733 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → Ord 𝐴) |
3 | | ordge1n0 7578 |
. . . . . . . . . 10
⊢ (Ord
𝐴 →
(1𝑜 ⊆ 𝐴 ↔ 𝐴 ≠ ∅)) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ On →
(1𝑜 ⊆ 𝐴 ↔ 𝐴 ≠ ∅)) |
5 | 4 | biimprd 238 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐴 ≠ ∅ →
1𝑜 ⊆ 𝐴)) |
6 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≠ ∅ →
1𝑜 ⊆ 𝐴)) |
7 | | on0eln0 5780 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
8 | 7 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
9 | | omword1 7653 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐵) → 𝐴 ⊆ (𝐴 ·𝑜 𝐵)) |
10 | 9 | ex 450 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐵 → 𝐴 ⊆ (𝐴 ·𝑜 𝐵))) |
11 | 8, 10 | sylbird 250 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ≠ ∅ → 𝐴 ⊆ (𝐴 ·𝑜 𝐵))) |
12 | 6, 11 | anim12d 586 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) →
(1𝑜 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ·𝑜 𝐵)))) |
13 | | sstr 3611 |
. . . . . 6
⊢
((1𝑜 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ·𝑜 𝐵)) → 1𝑜
⊆ (𝐴
·𝑜 𝐵)) |
14 | 12, 13 | syl6 35 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) →
1𝑜 ⊆ (𝐴 ·𝑜 𝐵))) |
15 | 1, 14 | syl5bir 233 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 = ∅ ∨ 𝐵 = ∅) →
1𝑜 ⊆ (𝐴 ·𝑜 𝐵))) |
16 | | omcl 7616 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
17 | | eloni 5733 |
. . . . 5
⊢ ((𝐴 ·𝑜
𝐵) ∈ On → Ord
(𝐴
·𝑜 𝐵)) |
18 | | ordge1n0 7578 |
. . . . 5
⊢ (Ord
(𝐴
·𝑜 𝐵) → (1𝑜 ⊆
(𝐴
·𝑜 𝐵) ↔ (𝐴 ·𝑜 𝐵) ≠
∅)) |
19 | 16, 17, 18 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1𝑜 ⊆ (𝐴 ·𝑜 𝐵) ↔ (𝐴 ·𝑜 𝐵) ≠
∅)) |
20 | 15, 19 | sylibd 229 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 ·𝑜
𝐵) ≠
∅)) |
21 | 20 | necon4bd 2814 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))) |
22 | | oveq1 6657 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) = (∅
·𝑜 𝐵)) |
23 | | om0r 7619 |
. . . . . 6
⊢ (𝐵 ∈ On → (∅
·𝑜 𝐵) = ∅) |
24 | 22, 23 | sylan9eqr 2678 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ·𝑜
𝐵) =
∅) |
25 | 24 | ex 450 |
. . . 4
⊢ (𝐵 ∈ On → (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
26 | 25 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
27 | | oveq2 6658 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ·𝑜
𝐵) = (𝐴 ·𝑜
∅)) |
28 | | om0 7597 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ·𝑜
∅) = ∅) |
29 | 27, 28 | sylan9eqr 2678 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ·𝑜
𝐵) =
∅) |
30 | 29 | ex 450 |
. . . 4
⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
31 | 30 | adantr 481 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
32 | 26, 31 | jaod 395 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 ·𝑜
𝐵) =
∅)) |
33 | 21, 32 | impbid 202 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) |