Proof of Theorem om00
Step | Hyp | Ref
| Expression |
1 | | neanior 3034 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ ¬
(𝐴 = ∅ ∨ 𝐵 = ∅)) |
2 | | eloni 6223 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → Ord 𝐴) |
3 | | ordge1n0 8225 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → (1o
⊆ 𝐴 ↔ 𝐴 ≠ ∅)) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (1o
⊆ 𝐴 ↔ 𝐴 ≠ ∅)) |
5 | 4 | biimprd 251 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐴 ≠ ∅ →
1o ⊆ 𝐴)) |
6 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≠ ∅ →
1o ⊆ 𝐴)) |
7 | | on0eln0 6268 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
8 | 7 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
9 | | omword1 8301 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐵) → 𝐴 ⊆ (𝐴 ·o 𝐵)) |
10 | 9 | ex 416 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐵 → 𝐴 ⊆ (𝐴 ·o 𝐵))) |
11 | 8, 10 | sylbird 263 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ≠ ∅ → 𝐴 ⊆ (𝐴 ·o 𝐵))) |
12 | 6, 11 | anim12d 612 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) →
(1o ⊆ 𝐴
∧ 𝐴 ⊆ (𝐴 ·o 𝐵)))) |
13 | | sstr 3909 |
. . . . . 6
⊢
((1o ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ·o 𝐵)) → 1o ⊆ (𝐴 ·o 𝐵)) |
14 | 12, 13 | syl6 35 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) →
1o ⊆ (𝐴
·o 𝐵))) |
15 | 1, 14 | syl5bir 246 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 = ∅ ∨ 𝐵 = ∅) → 1o
⊆ (𝐴
·o 𝐵))) |
16 | | omcl 8263 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
17 | | eloni 6223 |
. . . . 5
⊢ ((𝐴 ·o 𝐵) ∈ On → Ord (𝐴 ·o 𝐵)) |
18 | | ordge1n0 8225 |
. . . . 5
⊢ (Ord
(𝐴 ·o
𝐵) → (1o
⊆ (𝐴
·o 𝐵)
↔ (𝐴
·o 𝐵)
≠ ∅)) |
19 | 16, 17, 18 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1o ⊆ (𝐴
·o 𝐵)
↔ (𝐴
·o 𝐵)
≠ ∅)) |
20 | 15, 19 | sylibd 242 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 ·o 𝐵) ≠
∅)) |
21 | 20 | necon4bd 2960 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))) |
22 | | oveq1 7220 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ·o 𝐵) = (∅
·o 𝐵)) |
23 | | om0r 8266 |
. . . . . 6
⊢ (𝐵 ∈ On → (∅
·o 𝐵) =
∅) |
24 | 22, 23 | sylan9eqr 2800 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ·o 𝐵) = ∅) |
25 | 24 | ex 416 |
. . . 4
⊢ (𝐵 ∈ On → (𝐴 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
26 | 25 | adantl 485 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
27 | | oveq2 7221 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ·o 𝐵) = (𝐴 ·o
∅)) |
28 | | om0 8244 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) |
29 | 27, 28 | sylan9eqr 2800 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ·o 𝐵) = ∅) |
30 | 29 | ex 416 |
. . . 4
⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
31 | 30 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
32 | 26, 31 | jaod 859 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 ·o 𝐵) = ∅)) |
33 | 21, 32 | impbid 215 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) |