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

Theorem oeeui 8220
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 8221 gives an explicit expression for the unique solution of the equation, in terms of the solution 𝑃 to omeu 8203.) (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 4101 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
21adantr 483 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐴 ∈ On)
32ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ On)
4 simprl 769 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ On)
5 oecl 8154 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o 𝐶) ∈ On)
63, 4, 5syl2anc 586 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ∈ On)
7 om1 8160 . . . . . . . . . . . . . . 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 8108 . . . . . . . . . . . . . . . 16 1o = {∅}
10 dif1o 8117 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (𝐴 ∖ 1o) ↔ (𝐷𝐴𝐷 ≠ ∅))
1110simprbi 499 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷 ≠ ∅)
1211ad2antll 727 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ≠ ∅)
13 eldifi 4101 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷𝐴)
1413ad2antll 727 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷𝐴)
15 onelon 6209 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝐷𝐴) → 𝐷 ∈ On)
163, 14, 15syl2anc 586 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ∈ On)
17 on0eln0 6239 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ On → (∅ ∈ 𝐷𝐷 ≠ ∅))
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (∅ ∈ 𝐷𝐷 ≠ ∅))
1912, 18mpbird 259 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ 𝐷)
2019snssd 4734 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → {∅} ⊆ 𝐷)
219, 20eqsstrid 4013 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 1o𝐷)
22 1on 8101 . . . . . . . . . . . . . . . . 17 1o ∈ On
2322a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 1o ∈ On)
24 omwordi 8189 . . . . . . . . . . . . . . . 16 ((1o ∈ On ∧ 𝐷 ∈ On ∧ (𝐴o 𝐶) ∈ On) → (1o𝐷 → ((𝐴o 𝐶) ·o 1o) ⊆ ((𝐴o 𝐶) ·o 𝐷)))
2523, 16, 6, 24syl3anc 1366 . . . . . . . . . . . . . . 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 4004 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ⊆ ((𝐴o 𝐶) ·o 𝐷))
28 omcl 8153 . . . . . . . . . . . . . . . 16 (((𝐴o 𝐶) ∈ On ∧ 𝐷 ∈ On) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
296, 16, 28syl2anc 586 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
30 simplrl 775 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ (𝐴o 𝐶))
31 onelon 6209 . . . . . . . . . . . . . . . 16 (((𝐴o 𝐶) ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶)) → 𝐸 ∈ On)
326, 30, 31syl2anc 586 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ On)
33 oaword1 8170 . . . . . . . . . . . . . . 15 ((((𝐴o 𝐶) ·o 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
3429, 32, 33syl2anc 586 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
35 simplrr 776 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)
3634, 35sseqtrd 4005 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵)
3727, 36sstrd 3975 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ⊆ 𝐵)
38 oeeu.1 . . . . . . . . . . . . . . 15 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
3938oeeulem 8219 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)))
4039simp3d 1139 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝑋))
4140ad2antrr 724 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴o suc 𝑋))
4239simp1d 1137 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ On)
4342ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ On)
44 suceloni 7520 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → suc 𝑋 ∈ On)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝑋 ∈ On)
46 oecl 8154 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝑋 ∈ On) → (𝐴o suc 𝑋) ∈ On)
473, 45, 46syl2anc 586 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝑋) ∈ On)
48 ontr2 6231 . . . . . . . . . . . . 13 (((𝐴o 𝐶) ∈ On ∧ (𝐴o suc 𝑋) ∈ On) → (((𝐴o 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
496, 47, 48syl2anc 586 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
5037, 41, 49mp2and 697 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋))
51 simplll 773 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ (On ∖ 2o))
52 oeord 8206 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝐶 ∈ suc 𝑋 ↔ (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
534, 45, 51, 52syl3anc 1366 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 ∈ suc 𝑋 ↔ (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
5450, 53mpbird 259 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ suc 𝑋)
55 onsssuc 6271 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑋 ∈ On) → (𝐶𝑋𝐶 ∈ suc 𝑋))
564, 43, 55syl2anc 586 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶𝑋𝐶 ∈ suc 𝑋))
5754, 56mpbird 259 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶𝑋)
5839simp2d 1138 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ⊆ 𝐵)
5958ad2antrr 724 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ⊆ 𝐵)
60 eloni 6194 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → Ord 𝐴)
613, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → Ord 𝐴)
62 ordsucss 7525 . . . . . . . . . . . . . . . 16 (Ord 𝐴 → (𝐷𝐴 → suc 𝐷𝐴))
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷𝐴)
64 suceloni 7520 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ On → suc 𝐷 ∈ On)
6516, 64syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷 ∈ On)
66 dif20el 8122 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ 𝐴)
68 oen0 8204 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
693, 4, 67, 68syl21anc 835 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ (𝐴o 𝐶))
70 omword 8188 . . . . . . . . . . . . . . . 16 (((suc 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o 𝐶) ∈ On) ∧ ∅ ∈ (𝐴o 𝐶)) → (suc 𝐷𝐴 ↔ ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴)))
7165, 3, 6, 69, 70syl31anc 1368 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (suc 𝐷𝐴 ↔ ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴)))
7263, 71mpbid 234 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴))
73 oaord 8165 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ On ∧ (𝐴o 𝐶) ∈ On ∧ ((𝐴o 𝐶) ·o 𝐷) ∈ On) → (𝐸 ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶))))
7432, 6, 29, 73syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐸 ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶))))
7530, 74mpbid 234 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
7635, 75eqeltrrd 2912 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
77 odi 8197 . . . . . . . . . . . . . . . . 17 (((𝐴o 𝐶) ∈ On ∧ 𝐷 ∈ On ∧ 1o ∈ On) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)))
786, 16, 23, 77syl3anc 1366 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)))
79 oa1suc 8148 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ On → (𝐷 +o 1o) = suc 𝐷)
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐷 +o 1o) = suc 𝐷)
8180oveq2d 7164 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = ((𝐴o 𝐶) ·o suc 𝐷))
828oveq2d 7164 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
8378, 81, 823eqtr3d 2862 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o suc 𝐷) = (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
8476, 83eleqtrrd 2914 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴o 𝐶) ·o suc 𝐷))
8572, 84sseldd 3966 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴))
86 oesuc 8144 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
873, 4, 86syl2anc 586 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
8885, 87eleqtrrd 2914 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴o suc 𝐶))
89 oecl 8154 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
903, 43, 89syl2anc 586 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ∈ On)
91 suceloni 7520 . . . . . . . . . . . . . . 15 (𝐶 ∈ On → suc 𝐶 ∈ On)
9291ad2antrl 726 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐶 ∈ On)
93 oecl 8154 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴o suc 𝐶) ∈ On)
943, 92, 93syl2anc 586 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝐶) ∈ On)
95 ontr2 6231 . . . . . . . . . . . . 13 (((𝐴o 𝑋) ∈ On ∧ (𝐴o suc 𝐶) ∈ On) → (((𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝐶)) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9690, 94, 95syl2anc 586 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝐶)) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9759, 88, 96mp2and 697 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶))
98 oeord 8206 . . . . . . . . . . . 12 ((𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝑋 ∈ suc 𝐶 ↔ (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9943, 92, 51, 98syl3anc 1366 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋 ∈ suc 𝐶 ↔ (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
10097, 99mpbird 259 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ suc 𝐶)
101 onsssuc 6271 . . . . . . . . . . 11 ((𝑋 ∈ On ∧ 𝐶 ∈ On) → (𝑋𝐶𝑋 ∈ suc 𝐶))
10243, 4, 101syl2anc 586 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋𝐶𝑋 ∈ suc 𝐶))
103100, 102mpbird 259 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋𝐶)
10457, 103eqssd 3982 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 = 𝑋)
105104, 16jca 514 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 = 𝑋𝐷 ∈ On))
106 simprl 769 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 = 𝑋)
10742ad2antrr 724 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝑋 ∈ On)
108106, 107eqeltrd 2911 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 ∈ On)
1092ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐴 ∈ On)
110109, 108, 5syl2anc 586 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) ∈ On)
111 simprr 771 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ On)
112110, 111, 28syl2anc 586 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
113 simplrl 775 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ (𝐴o 𝐶))
114110, 113, 31syl2anc 586 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ On)
115112, 114, 33syl2anc 586 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
116 simplrr 776 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)
117115, 116sseqtrd 4005 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵)
11840ad2antrr 724 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ (𝐴o suc 𝑋))
119 suceq 6249 . . . . . . . . . . . . . . 15 (𝐶 = 𝑋 → suc 𝐶 = suc 𝑋)
120119ad2antrl 726 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → suc 𝐶 = suc 𝑋)
121120oveq2d 7164 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝐶) = (𝐴o suc 𝑋))
122109, 108, 86syl2anc 586 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
123121, 122eqtr3d 2856 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝑋) = ((𝐴o 𝐶) ·o 𝐴))
124118, 123eleqtrd 2913 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴))
125 omcl 8153 . . . . . . . . . . . . 13 (((𝐴o 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴o 𝐶) ·o 𝐴) ∈ On)
126110, 109, 125syl2anc 586 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐴) ∈ On)
127 ontr2 6231 . . . . . . . . . . . 12 ((((𝐴o 𝐶) ·o 𝐷) ∈ On ∧ ((𝐴o 𝐶) ·o 𝐴) ∈ On) → ((((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
128112, 126, 127syl2anc 586 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
129117, 124, 128mp2and 697 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴))
13066adantr 483 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∅ ∈ 𝐴)
131130ad2antrr 724 . . . . . . . . . . . 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 8185 . . . . . . . . . . 11 (((𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o 𝐶) ∈ On) ∧ ∅ ∈ (𝐴o 𝐶)) → (𝐷𝐴 ↔ ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
134111, 109, 110, 132, 133syl31anc 1368 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷𝐴 ↔ ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
135129, 134mpbird 259 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷𝐴)
136106oveq2d 7164 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) = (𝐴o 𝑋))
13758ad2antrr 724 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝑋) ⊆ 𝐵)
138136, 137eqsstrd 4003 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) ⊆ 𝐵)
139 eldifi 4101 . . . . . . . . . . . . . 14 (𝐵 ∈ (On ∖ 1o) → 𝐵 ∈ On)
140139adantl 484 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ On)
141140ad2antrr 724 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ On)
142 ontri1 6218 . . . . . . . . . . . 12 (((𝐴o 𝐶) ∈ On ∧ 𝐵 ∈ On) → ((𝐴o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝐶)))
143110, 141, 142syl2anc 586 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝐶)))
144138, 143mpbid 234 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ¬ 𝐵 ∈ (𝐴o 𝐶))
145 om0 8134 . . . . . . . . . . . . . . . . 17 ((𝐴o 𝐶) ∈ On → ((𝐴o 𝐶) ·o ∅) = ∅)
146110, 145syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o ∅) = ∅)
147146oveq1d 7163 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) = (∅ +o 𝐸))
148 oa0r 8155 . . . . . . . . . . . . . . . 16 (𝐸 ∈ On → (∅ +o 𝐸) = 𝐸)
149114, 148syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (∅ +o 𝐸) = 𝐸)
150147, 149eqtrd 2854 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) = 𝐸)
151150, 113eqeltrd 2911 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) ∈ (𝐴o 𝐶))
152 oveq2 7156 . . . . . . . . . . . . . . 15 (𝐷 = ∅ → ((𝐴o 𝐶) ·o 𝐷) = ((𝐴o 𝐶) ·o ∅))
153152oveq1d 7163 . . . . . . . . . . . . . 14 (𝐷 = ∅ → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴o 𝐶) ·o ∅) +o 𝐸))
154153eleq1d 2895 . . . . . . . . . . . . 13 (𝐷 = ∅ → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o ∅) +o 𝐸) ∈ (𝐴o 𝐶)))
155151, 154syl5ibrcom 249 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶)))
156116eleq1d 2895 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶) ↔ 𝐵 ∈ (𝐴o 𝐶)))
157155, 156sylibd 241 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → 𝐵 ∈ (𝐴o 𝐶)))
158157necon3bd 3028 . . . . . . . . . 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 585 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ (𝐴 ∖ 1o))
161108, 160jca 514 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)))
162105, 161impbida 799 . . . . . 6 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋𝐷 ∈ On)))
163162ex 415 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋𝐷 ∈ On))))
164163pm5.32rd 580 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ ((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))))
165 anass 471 . . . 4 (((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))))
166164, 165syl6bb 289 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))))
167 3anass 1090 . . . . . 6 ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))
168 oveq2 7156 . . . . . . . 8 (𝐶 = 𝑋 → (𝐴o 𝐶) = (𝐴o 𝑋))
169168eleq2d 2896 . . . . . . 7 (𝐶 = 𝑋 → (𝐸 ∈ (𝐴o 𝐶) ↔ 𝐸 ∈ (𝐴o 𝑋)))
170168oveq1d 7163 . . . . . . . . 9 (𝐶 = 𝑋 → ((𝐴o 𝐶) ·o 𝐷) = ((𝐴o 𝑋) ·o 𝐷))
171170oveq1d 7163 . . . . . . . 8 (𝐶 = 𝑋 → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴o 𝑋) ·o 𝐷) +o 𝐸))
172171eqeq1d 2821 . . . . . . 7 (𝐶 = 𝑋 → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))
173169, 1723anbi23d 1433 . . . . . 6 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)))
174167, 173syl5bbr 287 . . . . 5 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)))
1752, 42, 89syl2anc 586 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ∈ On)
176 oen0 8204 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝑋 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝑋))
1772, 42, 130, 176syl21anc 835 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∅ ∈ (𝐴o 𝑋))
178177ne0d 4299 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ≠ ∅)
179 omeu 8203 . . . . . . 7 (((𝐴o 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴o 𝑋) ≠ ∅) → ∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
180 oeeu.2 . . . . . . . . 9 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵))
181 opeq1 4795 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → ⟨𝑦, 𝑧⟩ = ⟨𝑑, 𝑧⟩)
182181eqeq2d 2830 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → (𝑤 = ⟨𝑦, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑧⟩))
183 oveq2 7156 . . . . . . . . . . . . . . 15 (𝑦 = 𝑑 → ((𝐴o 𝑋) ·o 𝑦) = ((𝐴o 𝑋) ·o 𝑑))
184183oveq1d 7163 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = (((𝐴o 𝑋) ·o 𝑑) +o 𝑧))
185184eqeq1d 2821 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → ((((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵))
186182, 185anbi12d 632 . . . . . . . . . . . 12 (𝑦 = 𝑑 → ((𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵)))
187 opeq2 4796 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → ⟨𝑑, 𝑧⟩ = ⟨𝑑, 𝑒⟩)
188187eqeq2d 2830 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → (𝑤 = ⟨𝑑, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑒⟩))
189 oveq2 7156 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = (((𝐴o 𝑋) ·o 𝑑) +o 𝑒))
190189eqeq1d 2821 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → ((((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
191188, 190anbi12d 632 . . . . . . . . . . . 12 (𝑧 = 𝑒 → ((𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
192186, 191cbvrex2vw 3461 . . . . . . . . . . 11 (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
193 eqeq1 2823 . . . . . . . . . . . . 13 (𝑤 = 𝑎 → (𝑤 = ⟨𝑑, 𝑒⟩ ↔ 𝑎 = ⟨𝑑, 𝑒⟩))
194193anbi1d 631 . . . . . . . . . . . 12 (𝑤 = 𝑎 → ((𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ (𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
1951942rexbidv 3298 . . . . . . . . . . 11 (𝑤 = 𝑎 → (∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
196192, 195syl5bb 285 . . . . . . . . . 10 (𝑤 = 𝑎 → (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
197196cbviotavw 6315 . . . . . . . . 9 (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵)) = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
198180, 197eqtri 2842 . . . . . . . 8 𝑃 = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
199 oeeu.3 . . . . . . . 8 𝑌 = (1st𝑃)
200 oeeu.4 . . . . . . . 8 𝑍 = (2nd𝑃)
201 oveq2 7156 . . . . . . . . . 10 (𝑑 = 𝐷 → ((𝐴o 𝑋) ·o 𝑑) = ((𝐴o 𝑋) ·o 𝐷))
202201oveq1d 7163 . . . . . . . . 9 (𝑑 = 𝐷 → (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = (((𝐴o 𝑋) ·o 𝐷) +o 𝑒))
203202eqeq1d 2821 . . . . . . . 8 (𝑑 = 𝐷 → ((((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵))
204 oveq2 7156 . . . . . . . . 9 (𝑒 = 𝐸 → (((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = (((𝐴o 𝑋) ·o 𝐷) +o 𝐸))
205204eqeq1d 2821 . . . . . . . 8 (𝑒 = 𝐸 → ((((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))
206198, 199, 200, 203, 205opiota 7749 . . . . . . 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 1366 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
209174, 208sylan9bbr 513 . . . 4 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ 𝐶 = 𝑋) → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
210209pm5.32da 581 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
211166, 210bitrd 281 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
212 3an4anass 1100 . 2 (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴o 𝐶)) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))
213 3anass 1090 . 2 ((𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍)))
214211, 212, 2133bitr4g 316 1 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴o 𝐶)) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  w3a 1082   = wceq 1531  wcel 2108  ∃!weu 2647  wne 3014  wrex 3137  {crab 3140  cdif 3931  wss 3934  c0 4289  {csn 4559  cop 4565   cuni 4830   cint 4867  Ord word 6183  Oncon0 6184  suc csuc 6186  cio 6305  cfv 6348  (class class class)co 7148  1st c1st 7679  2nd c2nd 7680  1oc1o 8087  2oc2o 8088   +o coa 8091   ·o comu 8092  o coe 8093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-omul 8099  df-oexp 8100
This theorem is referenced by:  oeeu  8221  cantnflem3  9146  cantnflem4  9147
  Copyright terms: Public domain W3C validator