Proof of Theorem omeulem2
| Step | Hyp | Ref
| Expression |
| 1 | | simp3l 1202 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐷 ∈ On) |
| 2 | | eloni 6394 |
. . . . . 6
⊢ (𝐷 ∈ On → Ord 𝐷) |
| 3 | | ordsucss 7838 |
. . . . . 6
⊢ (Ord
𝐷 → (𝐵 ∈ 𝐷 → suc 𝐵 ⊆ 𝐷)) |
| 4 | 1, 2, 3 | 3syl 18 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → suc 𝐵 ⊆ 𝐷)) |
| 5 | | simp2l 1200 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐵 ∈ On) |
| 6 | | onsuc 7831 |
. . . . . . 7
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
| 7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → suc 𝐵 ∈ On) |
| 8 | | simp1l 1198 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐴 ∈ On) |
| 9 | | simp1r 1199 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐴 ≠ ∅) |
| 10 | | on0eln0 6440 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 11 | 8, 10 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 12 | 9, 11 | mpbird 257 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ∅ ∈ 𝐴) |
| 13 | | omword 8608 |
. . . . . 6
⊢ (((suc
𝐵 ∈ On ∧ 𝐷 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (suc 𝐵 ⊆ 𝐷 ↔ (𝐴 ·o suc 𝐵) ⊆ (𝐴 ·o 𝐷))) |
| 14 | 7, 1, 8, 12, 13 | syl31anc 1375 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (suc 𝐵 ⊆ 𝐷 ↔ (𝐴 ·o suc 𝐵) ⊆ (𝐴 ·o 𝐷))) |
| 15 | 4, 14 | sylibd 239 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → (𝐴 ·o suc 𝐵) ⊆ (𝐴 ·o 𝐷))) |
| 16 | | omcl 8574 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐷 ∈ On) → (𝐴 ·o 𝐷) ∈ On) |
| 17 | 8, 1, 16 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐴 ·o 𝐷) ∈ On) |
| 18 | | simp3r 1203 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐸 ∈ 𝐴) |
| 19 | | onelon 6409 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐸 ∈ 𝐴) → 𝐸 ∈ On) |
| 20 | 8, 18, 19 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐸 ∈ On) |
| 21 | | oaword1 8590 |
. . . . . 6
⊢ (((𝐴 ·o 𝐷) ∈ On ∧ 𝐸 ∈ On) → (𝐴 ·o 𝐷) ⊆ ((𝐴 ·o 𝐷) +o 𝐸)) |
| 22 | | sstr 3992 |
. . . . . . 7
⊢ (((𝐴 ·o suc 𝐵) ⊆ (𝐴 ·o 𝐷) ∧ (𝐴 ·o 𝐷) ⊆ ((𝐴 ·o 𝐷) +o 𝐸)) → (𝐴 ·o suc 𝐵) ⊆ ((𝐴 ·o 𝐷) +o 𝐸)) |
| 23 | 22 | expcom 413 |
. . . . . 6
⊢ ((𝐴 ·o 𝐷) ⊆ ((𝐴 ·o 𝐷) +o 𝐸) → ((𝐴 ·o suc 𝐵) ⊆ (𝐴 ·o 𝐷) → (𝐴 ·o suc 𝐵) ⊆ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 24 | 21, 23 | syl 17 |
. . . . 5
⊢ (((𝐴 ·o 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴 ·o suc 𝐵) ⊆ (𝐴 ·o 𝐷) → (𝐴 ·o suc 𝐵) ⊆ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 25 | 17, 20, 24 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐴 ·o suc 𝐵) ⊆ (𝐴 ·o 𝐷) → (𝐴 ·o suc 𝐵) ⊆ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 26 | 15, 25 | syld 47 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → (𝐴 ·o suc 𝐵) ⊆ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 27 | | simp2r 1201 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐶 ∈ 𝐴) |
| 28 | | onelon 6409 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ On) |
| 29 | 8, 27, 28 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐶 ∈ On) |
| 30 | | omcl 8574 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
| 31 | 8, 5, 30 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐴 ·o 𝐵) ∈ On) |
| 32 | | oaord 8585 |
. . . . . 6
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) → (𝐶 ∈ 𝐴 ↔ ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐵) +o 𝐴))) |
| 33 | 32 | biimpa 476 |
. . . . 5
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) ∧ 𝐶 ∈ 𝐴) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐵) +o 𝐴)) |
| 34 | 29, 8, 31, 27, 33 | syl31anc 1375 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐵) +o 𝐴)) |
| 35 | | omsuc 8564 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) |
| 36 | 8, 5, 35 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) |
| 37 | 34, 36 | eleqtrrd 2844 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ (𝐴 ·o suc 𝐵)) |
| 38 | | ssel 3977 |
. . 3
⊢ ((𝐴 ·o suc 𝐵) ⊆ ((𝐴 ·o 𝐷) +o 𝐸) → (((𝐴 ·o 𝐵) +o 𝐶) ∈ (𝐴 ·o suc 𝐵) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 39 | 26, 37, 38 | syl6ci 71 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 40 | | simpr 484 |
. . . . 5
⊢ ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → 𝐶 ∈ 𝐸) |
| 41 | | oaord 8585 |
. . . . 5
⊢ ((𝐶 ∈ On ∧ 𝐸 ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) → (𝐶 ∈ 𝐸 ↔ ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐵) +o 𝐸))) |
| 42 | 40, 41 | imbitrid 244 |
. . . 4
⊢ ((𝐶 ∈ On ∧ 𝐸 ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) → ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐵) +o 𝐸))) |
| 43 | | oveq2 7439 |
. . . . . . 7
⊢ (𝐵 = 𝐷 → (𝐴 ·o 𝐵) = (𝐴 ·o 𝐷)) |
| 44 | 43 | oveq1d 7446 |
. . . . . 6
⊢ (𝐵 = 𝐷 → ((𝐴 ·o 𝐵) +o 𝐸) = ((𝐴 ·o 𝐷) +o 𝐸)) |
| 45 | 44 | adantr 480 |
. . . . 5
⊢ ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·o 𝐵) +o 𝐸) = ((𝐴 ·o 𝐷) +o 𝐸)) |
| 46 | 45 | eleq2d 2827 |
. . . 4
⊢ ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → (((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐵) +o 𝐸) ↔ ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 47 | 42, 46 | mpbidi 241 |
. . 3
⊢ ((𝐶 ∈ On ∧ 𝐸 ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) → ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 48 | 29, 20, 31, 47 | syl3anc 1373 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐷) +o 𝐸))) |
| 49 | 39, 48 | jaod 860 |
1
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐵 ∈ 𝐷 ∨ (𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸)) → ((𝐴 ·o 𝐵) +o 𝐶) ∈ ((𝐴 ·o 𝐷) +o 𝐸))) |