Proof of Theorem om00
| Step | Hyp | Ref
| Expression |
| 1 | | neanior 3035 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ ¬
(𝐴 = ∅ ∨ 𝐵 = ∅)) |
| 2 | | eloni 6394 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 3 | | ordge1n0 8532 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → (1o
⊆ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (1o
⊆ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 5 | 4 | biimprd 248 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐴 ≠ ∅ →
1o ⊆ 𝐴)) |
| 6 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≠ ∅ →
1o ⊆ 𝐴)) |
| 7 | | on0eln0 6440 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
| 8 | 7 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
| 9 | | omword1 8611 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐵) → 𝐴 ⊆ (𝐴 ·o 𝐵)) |
| 10 | 9 | ex 412 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐵 → 𝐴 ⊆ (𝐴 ·o 𝐵))) |
| 11 | 8, 10 | sylbird 260 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ≠ ∅ → 𝐴 ⊆ (𝐴 ·o 𝐵))) |
| 12 | 6, 11 | anim12d 609 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) →
(1o ⊆ 𝐴
∧ 𝐴 ⊆ (𝐴 ·o 𝐵)))) |
| 13 | | sstr 3992 |
. . . . . 6
⊢
((1o ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐴 ·o 𝐵)) → 1o ⊆ (𝐴 ·o 𝐵)) |
| 14 | 12, 13 | syl6 35 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) →
1o ⊆ (𝐴
·o 𝐵))) |
| 15 | 1, 14 | biimtrrid 243 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 = ∅ ∨ 𝐵 = ∅) → 1o
⊆ (𝐴
·o 𝐵))) |
| 16 | | omcl 8574 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
| 17 | | eloni 6394 |
. . . . 5
⊢ ((𝐴 ·o 𝐵) ∈ On → Ord (𝐴 ·o 𝐵)) |
| 18 | | ordge1n0 8532 |
. . . . 5
⊢ (Ord
(𝐴 ·o
𝐵) → (1o
⊆ (𝐴
·o 𝐵)
↔ (𝐴
·o 𝐵)
≠ ∅)) |
| 19 | 16, 17, 18 | 3syl 18 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(1o ⊆ (𝐴
·o 𝐵)
↔ (𝐴
·o 𝐵)
≠ ∅)) |
| 20 | 15, 19 | sylibd 239 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 ·o 𝐵) ≠
∅)) |
| 21 | 20 | necon4bd 2960 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))) |
| 22 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ·o 𝐵) = (∅
·o 𝐵)) |
| 23 | | om0r 8577 |
. . . . . 6
⊢ (𝐵 ∈ On → (∅
·o 𝐵) =
∅) |
| 24 | 22, 23 | sylan9eqr 2799 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴 ·o 𝐵) = ∅) |
| 25 | 24 | ex 412 |
. . . 4
⊢ (𝐵 ∈ On → (𝐴 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
| 26 | 25 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
| 27 | | oveq2 7439 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ·o 𝐵) = (𝐴 ·o
∅)) |
| 28 | | om0 8555 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) |
| 29 | 27, 28 | sylan9eqr 2799 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ·o 𝐵) = ∅) |
| 30 | 29 | ex 412 |
. . . 4
⊢ (𝐴 ∈ On → (𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
| 31 | 30 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅)) |
| 32 | 26, 31 | jaod 860 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 ·o 𝐵) = ∅)) |
| 33 | 21, 32 | impbid 212 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) |