MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oeeui Structured version   Visualization version   GIF version

Theorem oeeui 8597
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 8598 gives an explicit expression for the unique solution of the equation, in terms of the solution 𝑃 to omeu 8580.) (Contributed by Mario Carneiro, 25-May-2015.)
Hypotheses
Ref Expression
oeeu.1 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
oeeu.2 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵))
oeeu.3 𝑌 = (1st𝑃)
oeeu.4 𝑍 = (2nd𝑃)
Assertion
Ref Expression
oeeui ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴o 𝐶)) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍)))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐴   𝑤,𝐵,𝑥,𝑦,𝑧   𝑤,𝑋,𝑦,𝑧
Allowed substitution hints:   𝐶(𝑥,𝑦,𝑧,𝑤)   𝐷(𝑥,𝑦,𝑧,𝑤)   𝑃(𝑥,𝑦,𝑧,𝑤)   𝐸(𝑥,𝑦,𝑧,𝑤)   𝑋(𝑥)   𝑌(𝑥,𝑦,𝑧,𝑤)   𝑍(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem oeeui
Dummy variables 𝑎 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 4118 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
21adantr 480 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐴 ∈ On)
32ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ On)
4 simprl 768 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ On)
5 oecl 8532 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o 𝐶) ∈ On)
63, 4, 5syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ∈ On)
7 om1 8537 . . . . . . . . . . . . . . 15 ((𝐴o 𝐶) ∈ On → ((𝐴o 𝐶) ·o 1o) = (𝐴o 𝐶))
86, 7syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 1o) = (𝐴o 𝐶))
9 df1o2 8468 . . . . . . . . . . . . . . . 16 1o = {∅}
10 dif1o 8495 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (𝐴 ∖ 1o) ↔ (𝐷𝐴𝐷 ≠ ∅))
1110simprbi 496 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷 ≠ ∅)
1211ad2antll 726 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ≠ ∅)
13 eldifi 4118 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷𝐴)
1413ad2antll 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷𝐴)
15 onelon 6379 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝐷𝐴) → 𝐷 ∈ On)
163, 14, 15syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ∈ On)
17 on0eln0 6410 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ On → (∅ ∈ 𝐷𝐷 ≠ ∅))
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (∅ ∈ 𝐷𝐷 ≠ ∅))
1912, 18mpbird 257 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ 𝐷)
2019snssd 4804 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → {∅} ⊆ 𝐷)
219, 20eqsstrid 4022 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 1o𝐷)
22 1on 8473 . . . . . . . . . . . . . . . . 17 1o ∈ On
2322a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 1o ∈ On)
24 omwordi 8566 . . . . . . . . . . . . . . . 16 ((1o ∈ On ∧ 𝐷 ∈ On ∧ (𝐴o 𝐶) ∈ On) → (1o𝐷 → ((𝐴o 𝐶) ·o 1o) ⊆ ((𝐴o 𝐶) ·o 𝐷)))
2523, 16, 6, 24syl3anc 1368 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (1o𝐷 → ((𝐴o 𝐶) ·o 1o) ⊆ ((𝐴o 𝐶) ·o 𝐷)))
2621, 25mpd 15 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 1o) ⊆ ((𝐴o 𝐶) ·o 𝐷))
278, 26eqsstrrd 4013 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ⊆ ((𝐴o 𝐶) ·o 𝐷))
28 omcl 8531 . . . . . . . . . . . . . . . 16 (((𝐴o 𝐶) ∈ On ∧ 𝐷 ∈ On) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
296, 16, 28syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
30 simplrl 774 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ (𝐴o 𝐶))
31 onelon 6379 . . . . . . . . . . . . . . . 16 (((𝐴o 𝐶) ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶)) → 𝐸 ∈ On)
326, 30, 31syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ On)
33 oaword1 8547 . . . . . . . . . . . . . . 15 ((((𝐴o 𝐶) ·o 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
3429, 32, 33syl2anc 583 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
35 simplrr 775 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)
3634, 35sseqtrd 4014 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵)
3727, 36sstrd 3984 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ⊆ 𝐵)
38 oeeu.1 . . . . . . . . . . . . . . 15 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
3938oeeulem 8596 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)))
4039simp3d 1141 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝑋))
4140ad2antrr 723 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴o suc 𝑋))
4239simp1d 1139 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ On)
4342ad2antrr 723 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ On)
44 onsuc 7792 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → suc 𝑋 ∈ On)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝑋 ∈ On)
46 oecl 8532 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝑋 ∈ On) → (𝐴o suc 𝑋) ∈ On)
473, 45, 46syl2anc 583 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝑋) ∈ On)
48 ontr2 6401 . . . . . . . . . . . . 13 (((𝐴o 𝐶) ∈ On ∧ (𝐴o suc 𝑋) ∈ On) → (((𝐴o 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
496, 47, 48syl2anc 583 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
5037, 41, 49mp2and 696 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋))
51 simplll 772 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ (On ∖ 2o))
52 oeord 8583 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝐶 ∈ suc 𝑋 ↔ (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
534, 45, 51, 52syl3anc 1368 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 ∈ suc 𝑋 ↔ (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
5450, 53mpbird 257 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ suc 𝑋)
55 onsssuc 6444 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑋 ∈ On) → (𝐶𝑋𝐶 ∈ suc 𝑋))
564, 43, 55syl2anc 583 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶𝑋𝐶 ∈ suc 𝑋))
5754, 56mpbird 257 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶𝑋)
5839simp2d 1140 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ⊆ 𝐵)
5958ad2antrr 723 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ⊆ 𝐵)
60 eloni 6364 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → Ord 𝐴)
613, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → Ord 𝐴)
62 ordsucss 7799 . . . . . . . . . . . . . . . 16 (Ord 𝐴 → (𝐷𝐴 → suc 𝐷𝐴))
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷𝐴)
64 onsuc 7792 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ On → suc 𝐷 ∈ On)
6516, 64syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷 ∈ On)
66 dif20el 8500 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ 𝐴)
68 oen0 8581 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
693, 4, 67, 68syl21anc 835 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ (𝐴o 𝐶))
70 omword 8565 . . . . . . . . . . . . . . . 16 (((suc 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o 𝐶) ∈ On) ∧ ∅ ∈ (𝐴o 𝐶)) → (suc 𝐷𝐴 ↔ ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴)))
7165, 3, 6, 69, 70syl31anc 1370 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (suc 𝐷𝐴 ↔ ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴)))
7263, 71mpbid 231 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴))
73 oaord 8542 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ On ∧ (𝐴o 𝐶) ∈ On ∧ ((𝐴o 𝐶) ·o 𝐷) ∈ On) → (𝐸 ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶))))
7432, 6, 29, 73syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐸 ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶))))
7530, 74mpbid 231 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
7635, 75eqeltrrd 2826 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
77 odi 8574 . . . . . . . . . . . . . . . . 17 (((𝐴o 𝐶) ∈ On ∧ 𝐷 ∈ On ∧ 1o ∈ On) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)))
786, 16, 23, 77syl3anc 1368 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)))
79 oa1suc 8526 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ On → (𝐷 +o 1o) = suc 𝐷)
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐷 +o 1o) = suc 𝐷)
8180oveq2d 7417 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = ((𝐴o 𝐶) ·o suc 𝐷))
828oveq2d 7417 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
8378, 81, 823eqtr3d 2772 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o suc 𝐷) = (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
8476, 83eleqtrrd 2828 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴o 𝐶) ·o suc 𝐷))
8572, 84sseldd 3975 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴))
86 oesuc 8522 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
873, 4, 86syl2anc 583 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
8885, 87eleqtrrd 2828 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴o suc 𝐶))
89 oecl 8532 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
903, 43, 89syl2anc 583 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ∈ On)
91 onsuc 7792 . . . . . . . . . . . . . . 15 (𝐶 ∈ On → suc 𝐶 ∈ On)
9291ad2antrl 725 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐶 ∈ On)
93 oecl 8532 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴o suc 𝐶) ∈ On)
943, 92, 93syl2anc 583 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝐶) ∈ On)
95 ontr2 6401 . . . . . . . . . . . . 13 (((𝐴o 𝑋) ∈ On ∧ (𝐴o suc 𝐶) ∈ On) → (((𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝐶)) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9690, 94, 95syl2anc 583 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝐶)) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9759, 88, 96mp2and 696 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶))
98 oeord 8583 . . . . . . . . . . . 12 ((𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝑋 ∈ suc 𝐶 ↔ (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9943, 92, 51, 98syl3anc 1368 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋 ∈ suc 𝐶 ↔ (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
10097, 99mpbird 257 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ suc 𝐶)
101 onsssuc 6444 . . . . . . . . . . 11 ((𝑋 ∈ On ∧ 𝐶 ∈ On) → (𝑋𝐶𝑋 ∈ suc 𝐶))
10243, 4, 101syl2anc 583 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋𝐶𝑋 ∈ suc 𝐶))
103100, 102mpbird 257 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋𝐶)
10457, 103eqssd 3991 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 = 𝑋)
105104, 16jca 511 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 = 𝑋𝐷 ∈ On))
106 simprl 768 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 = 𝑋)
10742ad2antrr 723 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝑋 ∈ On)
108106, 107eqeltrd 2825 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 ∈ On)
1092ad2antrr 723 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐴 ∈ On)
110109, 108, 5syl2anc 583 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) ∈ On)
111 simprr 770 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ On)
112110, 111, 28syl2anc 583 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
113 simplrl 774 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ (𝐴o 𝐶))
114110, 113, 31syl2anc 583 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ On)
115112, 114, 33syl2anc 583 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
116 simplrr 775 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)
117115, 116sseqtrd 4014 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵)
11840ad2antrr 723 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ (𝐴o suc 𝑋))
119 suceq 6420 . . . . . . . . . . . . . . 15 (𝐶 = 𝑋 → suc 𝐶 = suc 𝑋)
120119ad2antrl 725 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → suc 𝐶 = suc 𝑋)
121120oveq2d 7417 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝐶) = (𝐴o suc 𝑋))
122109, 108, 86syl2anc 583 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
123121, 122eqtr3d 2766 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝑋) = ((𝐴o 𝐶) ·o 𝐴))
124118, 123eleqtrd 2827 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴))
125 omcl 8531 . . . . . . . . . . . . 13 (((𝐴o 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴o 𝐶) ·o 𝐴) ∈ On)
126110, 109, 125syl2anc 583 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐴) ∈ On)
127 ontr2 6401 . . . . . . . . . . . 12 ((((𝐴o 𝐶) ·o 𝐷) ∈ On ∧ ((𝐴o 𝐶) ·o 𝐴) ∈ On) → ((((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
128112, 126, 127syl2anc 583 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
129117, 124, 128mp2and 696 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴))
13066adantr 480 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∅ ∈ 𝐴)
131130ad2antrr 723 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ 𝐴)
132109, 108, 131, 68syl21anc 835 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ (𝐴o 𝐶))
133 omord2 8562 . . . . . . . . . . 11 (((𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o 𝐶) ∈ On) ∧ ∅ ∈ (𝐴o 𝐶)) → (𝐷𝐴 ↔ ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
134111, 109, 110, 132, 133syl31anc 1370 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷𝐴 ↔ ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
135129, 134mpbird 257 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷𝐴)
136106oveq2d 7417 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) = (𝐴o 𝑋))
13758ad2antrr 723 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝑋) ⊆ 𝐵)
138136, 137eqsstrd 4012 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) ⊆ 𝐵)
139 eldifi 4118 . . . . . . . . . . . . . 14 (𝐵 ∈ (On ∖ 1o) → 𝐵 ∈ On)
140139adantl 481 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ On)
141140ad2antrr 723 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ On)
142 ontri1 6388 . . . . . . . . . . . 12 (((𝐴o 𝐶) ∈ On ∧ 𝐵 ∈ On) → ((𝐴o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝐶)))
143110, 141, 142syl2anc 583 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝐶)))
144138, 143mpbid 231 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ¬ 𝐵 ∈ (𝐴o 𝐶))
145 om0 8512 . . . . . . . . . . . . . . . . 17 ((𝐴o 𝐶) ∈ On → ((𝐴o 𝐶) ·o ∅) = ∅)
146110, 145syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o ∅) = ∅)
147146oveq1d 7416 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) = (∅ +o 𝐸))
148 oa0r 8533 . . . . . . . . . . . . . . . 16 (𝐸 ∈ On → (∅ +o 𝐸) = 𝐸)
149114, 148syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (∅ +o 𝐸) = 𝐸)
150147, 149eqtrd 2764 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) = 𝐸)
151150, 113eqeltrd 2825 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) ∈ (𝐴o 𝐶))
152 oveq2 7409 . . . . . . . . . . . . . . 15 (𝐷 = ∅ → ((𝐴o 𝐶) ·o 𝐷) = ((𝐴o 𝐶) ·o ∅))
153152oveq1d 7416 . . . . . . . . . . . . . 14 (𝐷 = ∅ → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴o 𝐶) ·o ∅) +o 𝐸))
154153eleq1d 2810 . . . . . . . . . . . . 13 (𝐷 = ∅ → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o ∅) +o 𝐸) ∈ (𝐴o 𝐶)))
155151, 154syl5ibrcom 246 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶)))
156116eleq1d 2810 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶) ↔ 𝐵 ∈ (𝐴o 𝐶)))
157155, 156sylibd 238 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → 𝐵 ∈ (𝐴o 𝐶)))
158157necon3bd 2946 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (¬ 𝐵 ∈ (𝐴o 𝐶) → 𝐷 ≠ ∅))
159144, 158mpd 15 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ≠ ∅)
160135, 159, 10sylanbrc 582 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ (𝐴 ∖ 1o))
161108, 160jca 511 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)))
162105, 161impbida 798 . . . . . 6 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋𝐷 ∈ On)))
163162ex 412 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋𝐷 ∈ On))))
164163pm5.32rd 577 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ ((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))))
165 anass 468 . . . 4 (((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))))
166164, 165bitrdi 287 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))))
167 3anass 1092 . . . . . 6 ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))
168 oveq2 7409 . . . . . . . 8 (𝐶 = 𝑋 → (𝐴o 𝐶) = (𝐴o 𝑋))
169168eleq2d 2811 . . . . . . 7 (𝐶 = 𝑋 → (𝐸 ∈ (𝐴o 𝐶) ↔ 𝐸 ∈ (𝐴o 𝑋)))
170168oveq1d 7416 . . . . . . . . 9 (𝐶 = 𝑋 → ((𝐴o 𝐶) ·o 𝐷) = ((𝐴o 𝑋) ·o 𝐷))
171170oveq1d 7416 . . . . . . . 8 (𝐶 = 𝑋 → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴o 𝑋) ·o 𝐷) +o 𝐸))
172171eqeq1d 2726 . . . . . . 7 (𝐶 = 𝑋 → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))
173169, 1723anbi23d 1435 . . . . . 6 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)))
174167, 173bitr3id 285 . . . . 5 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)))
1752, 42, 89syl2anc 583 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ∈ On)
176 oen0 8581 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝑋 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝑋))
1772, 42, 130, 176syl21anc 835 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∅ ∈ (𝐴o 𝑋))
178177ne0d 4327 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ≠ ∅)
179 omeu 8580 . . . . . . 7 (((𝐴o 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴o 𝑋) ≠ ∅) → ∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
180 oeeu.2 . . . . . . . . 9 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵))
181 opeq1 4865 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → ⟨𝑦, 𝑧⟩ = ⟨𝑑, 𝑧⟩)
182181eqeq2d 2735 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → (𝑤 = ⟨𝑦, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑧⟩))
183 oveq2 7409 . . . . . . . . . . . . . . 15 (𝑦 = 𝑑 → ((𝐴o 𝑋) ·o 𝑦) = ((𝐴o 𝑋) ·o 𝑑))
184183oveq1d 7416 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = (((𝐴o 𝑋) ·o 𝑑) +o 𝑧))
185184eqeq1d 2726 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → ((((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵))
186182, 185anbi12d 630 . . . . . . . . . . . 12 (𝑦 = 𝑑 → ((𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵)))
187 opeq2 4866 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → ⟨𝑑, 𝑧⟩ = ⟨𝑑, 𝑒⟩)
188187eqeq2d 2735 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → (𝑤 = ⟨𝑑, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑒⟩))
189 oveq2 7409 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = (((𝐴o 𝑋) ·o 𝑑) +o 𝑒))
190189eqeq1d 2726 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → ((((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
191188, 190anbi12d 630 . . . . . . . . . . . 12 (𝑧 = 𝑒 → ((𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
192186, 191cbvrex2vw 3231 . . . . . . . . . . 11 (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
193 eqeq1 2728 . . . . . . . . . . . . 13 (𝑤 = 𝑎 → (𝑤 = ⟨𝑑, 𝑒⟩ ↔ 𝑎 = ⟨𝑑, 𝑒⟩))
194193anbi1d 629 . . . . . . . . . . . 12 (𝑤 = 𝑎 → ((𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ (𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
1951942rexbidv 3211 . . . . . . . . . . 11 (𝑤 = 𝑎 → (∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
196192, 195bitrid 283 . . . . . . . . . 10 (𝑤 = 𝑎 → (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
197196cbviotavw 6493 . . . . . . . . 9 (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵)) = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
198180, 197eqtri 2752 . . . . . . . 8 𝑃 = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
199 oeeu.3 . . . . . . . 8 𝑌 = (1st𝑃)
200 oeeu.4 . . . . . . . 8 𝑍 = (2nd𝑃)
201 oveq2 7409 . . . . . . . . . 10 (𝑑 = 𝐷 → ((𝐴o 𝑋) ·o 𝑑) = ((𝐴o 𝑋) ·o 𝐷))
202201oveq1d 7416 . . . . . . . . 9 (𝑑 = 𝐷 → (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = (((𝐴o 𝑋) ·o 𝐷) +o 𝑒))
203202eqeq1d 2726 . . . . . . . 8 (𝑑 = 𝐷 → ((((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵))
204 oveq2 7409 . . . . . . . . 9 (𝑒 = 𝐸 → (((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = (((𝐴o 𝑋) ·o 𝐷) +o 𝐸))
205204eqeq1d 2726 . . . . . . . 8 (𝑒 = 𝐸 → ((((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))
206198, 199, 200, 203, 205opiota 8038 . . . . . . 7 (∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
207179, 206syl 17 . . . . . 6 (((𝐴o 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴o 𝑋) ≠ ∅) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
208175, 140, 178, 207syl3anc 1368 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
209174, 208sylan9bbr 510 . . . 4 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ 𝐶 = 𝑋) → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
210209pm5.32da 578 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
211166, 210bitrd 279 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
212 3an4anass 1102 . 2 (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴o 𝐶)) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))
213 3anass 1092 . 2 ((𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍)))
214211, 212, 2133bitr4g 314 1 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴o 𝐶)) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  ∃!weu 2554  wne 2932  wrex 3062  {crab 3424  cdif 3937  wss 3940  c0 4314  {csn 4620  cop 4626   cuni 4899   cint 4940  Ord word 6353  Oncon0 6354  suc csuc 6356  cio 6483  cfv 6533  (class class class)co 7401  1st c1st 7966  2nd c2nd 7967  1oc1o 8454  2oc2o 8455   +o coa 8458   ·o comu 8459  o coe 8460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-omul 8466  df-oexp 8467
This theorem is referenced by:  oeeu  8598  cantnflem3  9682  cantnflem4  9683
  Copyright terms: Public domain W3C validator