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

Theorem oeeui 7949
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 7950 gives an explicit expression for the unique solution of the equation, in terms of the solution 𝑃 to omeu 7932.) (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 3959 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
21adantr 474 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐴 ∈ On)
32ad2antrr 719 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ On)
4 simprl 789 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ On)
5 oecl 7884 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o 𝐶) ∈ On)
63, 4, 5syl2anc 581 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ∈ On)
7 om1 7889 . . . . . . . . . . . . . . 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 7839 . . . . . . . . . . . . . . . 16 1o = {∅}
10 dif1o 7847 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (𝐴 ∖ 1o) ↔ (𝐷𝐴𝐷 ≠ ∅))
1110simprbi 492 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷 ≠ ∅)
1211ad2antll 722 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ≠ ∅)
13 eldifi 3959 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷𝐴)
1413ad2antll 722 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷𝐴)
15 onelon 5988 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝐷𝐴) → 𝐷 ∈ On)
163, 14, 15syl2anc 581 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ∈ On)
17 on0eln0 6018 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ On → (∅ ∈ 𝐷𝐷 ≠ ∅))
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (∅ ∈ 𝐷𝐷 ≠ ∅))
1912, 18mpbird 249 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ 𝐷)
2019snssd 4558 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → {∅} ⊆ 𝐷)
219, 20syl5eqss 3874 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 1o𝐷)
22 1on 7833 . . . . . . . . . . . . . . . . 17 1o ∈ On
2322a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 1o ∈ On)
24 omwordi 7918 . . . . . . . . . . . . . . . 16 ((1o ∈ On ∧ 𝐷 ∈ On ∧ (𝐴o 𝐶) ∈ On) → (1o𝐷 → ((𝐴o 𝐶) ·o 1o) ⊆ ((𝐴o 𝐶) ·o 𝐷)))
2523, 16, 6, 24syl3anc 1496 . . . . . . . . . . . . . . 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, 26eqsstr3d 3865 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ⊆ ((𝐴o 𝐶) ·o 𝐷))
28 omcl 7883 . . . . . . . . . . . . . . . 16 (((𝐴o 𝐶) ∈ On ∧ 𝐷 ∈ On) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
296, 16, 28syl2anc 581 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
30 simplrl 797 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ (𝐴o 𝐶))
31 onelon 5988 . . . . . . . . . . . . . . . 16 (((𝐴o 𝐶) ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶)) → 𝐸 ∈ On)
326, 30, 31syl2anc 581 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ On)
33 oaword1 7899 . . . . . . . . . . . . . . 15 ((((𝐴o 𝐶) ·o 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
3429, 32, 33syl2anc 581 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
35 simplrr 798 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)
3634, 35sseqtrd 3866 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵)
3727, 36sstrd 3837 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ⊆ 𝐵)
38 oeeu.1 . . . . . . . . . . . . . . 15 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴o 𝑥)}
3938oeeulem 7948 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)))
4039simp3d 1180 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴o suc 𝑋))
4140ad2antrr 719 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴o suc 𝑋))
4239simp1d 1178 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝑋 ∈ On)
4342ad2antrr 719 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ On)
44 suceloni 7274 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → suc 𝑋 ∈ On)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝑋 ∈ On)
46 oecl 7884 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝑋 ∈ On) → (𝐴o suc 𝑋) ∈ On)
473, 45, 46syl2anc 581 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝑋) ∈ On)
48 ontr2 6010 . . . . . . . . . . . . 13 (((𝐴o 𝐶) ∈ On ∧ (𝐴o suc 𝑋) ∈ On) → (((𝐴o 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
496, 47, 48syl2anc 581 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝑋)) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
5037, 41, 49mp2and 692 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝐶) ∈ (𝐴o suc 𝑋))
51 simplll 793 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ (On ∖ 2o))
52 oeord 7935 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝐶 ∈ suc 𝑋 ↔ (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
534, 45, 51, 52syl3anc 1496 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 ∈ suc 𝑋 ↔ (𝐴o 𝐶) ∈ (𝐴o suc 𝑋)))
5450, 53mpbird 249 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ suc 𝑋)
55 onsssuc 6050 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑋 ∈ On) → (𝐶𝑋𝐶 ∈ suc 𝑋))
564, 43, 55syl2anc 581 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶𝑋𝐶 ∈ suc 𝑋))
5754, 56mpbird 249 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶𝑋)
5839simp2d 1179 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ⊆ 𝐵)
5958ad2antrr 719 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ⊆ 𝐵)
60 eloni 5973 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → Ord 𝐴)
613, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → Ord 𝐴)
62 ordsucss 7279 . . . . . . . . . . . . . . . 16 (Ord 𝐴 → (𝐷𝐴 → suc 𝐷𝐴))
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷𝐴)
64 suceloni 7274 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ On → suc 𝐷 ∈ On)
6516, 64syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷 ∈ On)
66 dif20el 7852 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ 𝐴)
68 oen0 7933 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
693, 4, 67, 68syl21anc 873 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅ ∈ (𝐴o 𝐶))
70 omword 7917 . . . . . . . . . . . . . . . 16 (((suc 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o 𝐶) ∈ On) ∧ ∅ ∈ (𝐴o 𝐶)) → (suc 𝐷𝐴 ↔ ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴)))
7165, 3, 6, 69, 70syl31anc 1498 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (suc 𝐷𝐴 ↔ ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴)))
7263, 71mpbid 224 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o suc 𝐷) ⊆ ((𝐴o 𝐶) ·o 𝐴))
73 oaord 7894 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ On ∧ (𝐴o 𝐶) ∈ On ∧ ((𝐴o 𝐶) ·o 𝐷) ∈ On) → (𝐸 ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶))))
7432, 6, 29, 73syl3anc 1496 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐸 ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶))))
7530, 74mpbid 224 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
7635, 75eqeltrrd 2907 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
77 odi 7926 . . . . . . . . . . . . . . . . 17 (((𝐴o 𝐶) ∈ On ∧ 𝐷 ∈ On ∧ 1o ∈ On) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)))
786, 16, 23, 77syl3anc 1496 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)))
79 oa1suc 7878 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ On → (𝐷 +o 1o) = suc 𝐷)
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐷 +o 1o) = suc 𝐷)
8180oveq2d 6921 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o (𝐷 +o 1o)) = ((𝐴o 𝐶) ·o suc 𝐷))
828oveq2d 6921 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝐶) ·o 𝐷) +o ((𝐴o 𝐶) ·o 1o)) = (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
8378, 81, 823eqtr3d 2869 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴o 𝐶) ·o suc 𝐷) = (((𝐴o 𝐶) ·o 𝐷) +o (𝐴o 𝐶)))
8476, 83eleqtrrd 2909 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴o 𝐶) ·o suc 𝐷))
8572, 84sseldd 3828 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴))
86 oesuc 7874 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
873, 4, 86syl2anc 581 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
8885, 87eleqtrrd 2909 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴o suc 𝐶))
89 oecl 7884 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
903, 43, 89syl2anc 581 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ∈ On)
91 suceloni 7274 . . . . . . . . . . . . . . 15 (𝐶 ∈ On → suc 𝐶 ∈ On)
9291ad2antrl 721 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐶 ∈ On)
93 oecl 7884 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴o suc 𝐶) ∈ On)
943, 92, 93syl2anc 581 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o suc 𝐶) ∈ On)
95 ontr2 6010 . . . . . . . . . . . . 13 (((𝐴o 𝑋) ∈ On ∧ (𝐴o suc 𝐶) ∈ On) → (((𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝐶)) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9690, 94, 95syl2anc 581 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴o 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴o suc 𝐶)) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9759, 88, 96mp2and 692 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴o 𝑋) ∈ (𝐴o suc 𝐶))
98 oeord 7935 . . . . . . . . . . . 12 ((𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝑋 ∈ suc 𝐶 ↔ (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
9943, 92, 51, 98syl3anc 1496 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋 ∈ suc 𝐶 ↔ (𝐴o 𝑋) ∈ (𝐴o suc 𝐶)))
10097, 99mpbird 249 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ suc 𝐶)
101 onsssuc 6050 . . . . . . . . . . 11 ((𝑋 ∈ On ∧ 𝐶 ∈ On) → (𝑋𝐶𝑋 ∈ suc 𝐶))
10243, 4, 101syl2anc 581 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋𝐶𝑋 ∈ suc 𝐶))
103100, 102mpbird 249 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋𝐶)
10457, 103eqssd 3844 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 = 𝑋)
105104, 16jca 509 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 = 𝑋𝐷 ∈ On))
106 simprl 789 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 = 𝑋)
10742ad2antrr 719 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝑋 ∈ On)
108106, 107eqeltrd 2906 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 ∈ On)
1092ad2antrr 719 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐴 ∈ On)
110109, 108, 5syl2anc 581 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) ∈ On)
111 simprr 791 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ On)
112110, 111, 28syl2anc 581 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ∈ On)
113 simplrl 797 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ (𝐴o 𝐶))
114110, 113, 31syl2anc 581 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ On)
115112, 114, 33syl2anc 581 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ⊆ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸))
116 simplrr 798 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)
117115, 116sseqtrd 3866 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵)
11840ad2antrr 719 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ (𝐴o suc 𝑋))
119 suceq 6028 . . . . . . . . . . . . . . 15 (𝐶 = 𝑋 → suc 𝐶 = suc 𝑋)
120119ad2antrl 721 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → suc 𝐶 = suc 𝑋)
121120oveq2d 6921 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝐶) = (𝐴o suc 𝑋))
122109, 108, 86syl2anc 581 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝐶) = ((𝐴o 𝐶) ·o 𝐴))
123121, 122eqtr3d 2863 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o suc 𝑋) = ((𝐴o 𝐶) ·o 𝐴))
124118, 123eleqtrd 2908 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴))
125 omcl 7883 . . . . . . . . . . . . 13 (((𝐴o 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴o 𝐶) ·o 𝐴) ∈ On)
126110, 109, 125syl2anc 581 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐴) ∈ On)
127 ontr2 6010 . . . . . . . . . . . 12 ((((𝐴o 𝐶) ·o 𝐷) ∈ On ∧ ((𝐴o 𝐶) ·o 𝐴) ∈ On) → ((((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
128112, 126, 127syl2anc 581 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴o 𝐶) ·o 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴o 𝐶) ·o 𝐴)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
129117, 124, 128mp2and 692 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴))
13066adantr 474 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∅ ∈ 𝐴)
131130ad2antrr 719 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ 𝐴)
132109, 108, 131, 68syl21anc 873 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ (𝐴o 𝐶))
133 omord2 7914 . . . . . . . . . . 11 (((𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o 𝐶) ∈ On) ∧ ∅ ∈ (𝐴o 𝐶)) → (𝐷𝐴 ↔ ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
134111, 109, 110, 132, 133syl31anc 1498 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷𝐴 ↔ ((𝐴o 𝐶) ·o 𝐷) ∈ ((𝐴o 𝐶) ·o 𝐴)))
135129, 134mpbird 249 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷𝐴)
136106oveq2d 6921 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) = (𝐴o 𝑋))
13758ad2antrr 719 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝑋) ⊆ 𝐵)
138136, 137eqsstrd 3864 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴o 𝐶) ⊆ 𝐵)
139 eldifi 3959 . . . . . . . . . . . . . 14 (𝐵 ∈ (On ∖ 1o) → 𝐵 ∈ On)
140139adantl 475 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → 𝐵 ∈ On)
141140ad2antrr 719 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ On)
142 ontri1 5997 . . . . . . . . . . . 12 (((𝐴o 𝐶) ∈ On ∧ 𝐵 ∈ On) → ((𝐴o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝐶)))
143110, 141, 142syl2anc 581 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴o 𝐶)))
144138, 143mpbid 224 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ¬ 𝐵 ∈ (𝐴o 𝐶))
145 om0 7864 . . . . . . . . . . . . . . . . 17 ((𝐴o 𝐶) ∈ On → ((𝐴o 𝐶) ·o ∅) = ∅)
146110, 145syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴o 𝐶) ·o ∅) = ∅)
147146oveq1d 6920 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) = (∅ +o 𝐸))
148 oa0r 7885 . . . . . . . . . . . . . . . 16 (𝐸 ∈ On → (∅ +o 𝐸) = 𝐸)
149114, 148syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (∅ +o 𝐸) = 𝐸)
150147, 149eqtrd 2861 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) = 𝐸)
151150, 113eqeltrd 2906 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴o 𝐶) ·o ∅) +o 𝐸) ∈ (𝐴o 𝐶))
152 oveq2 6913 . . . . . . . . . . . . . . 15 (𝐷 = ∅ → ((𝐴o 𝐶) ·o 𝐷) = ((𝐴o 𝐶) ·o ∅))
153152oveq1d 6920 . . . . . . . . . . . . . 14 (𝐷 = ∅ → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴o 𝐶) ·o ∅) +o 𝐸))
154153eleq1d 2891 . . . . . . . . . . . . 13 (𝐷 = ∅ → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶) ↔ (((𝐴o 𝐶) ·o ∅) +o 𝐸) ∈ (𝐴o 𝐶)))
155151, 154syl5ibrcom 239 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶)))
156116eleq1d 2891 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴o 𝐶) ↔ 𝐵 ∈ (𝐴o 𝐶)))
157155, 156sylibd 231 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → 𝐵 ∈ (𝐴o 𝐶)))
158157necon3bd 3013 . . . . . . . . . 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 580 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ (𝐴 ∖ 1o))
161108, 160jca 509 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)))
162105, 161impbida 837 . . . . . 6 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋𝐷 ∈ On)))
163162ex 403 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋𝐷 ∈ On))))
164163pm5.32rd 575 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ ((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))))
165 anass 462 . . . 4 (((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))))
166164, 165syl6bb 279 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))))
167 3anass 1122 . . . . . 6 ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))
168 oveq2 6913 . . . . . . . 8 (𝐶 = 𝑋 → (𝐴o 𝐶) = (𝐴o 𝑋))
169168eleq2d 2892 . . . . . . 7 (𝐶 = 𝑋 → (𝐸 ∈ (𝐴o 𝐶) ↔ 𝐸 ∈ (𝐴o 𝑋)))
170168oveq1d 6920 . . . . . . . . 9 (𝐶 = 𝑋 → ((𝐴o 𝐶) ·o 𝐷) = ((𝐴o 𝑋) ·o 𝐷))
171170oveq1d 6920 . . . . . . . 8 (𝐶 = 𝑋 → (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴o 𝑋) ·o 𝐷) +o 𝐸))
172171eqeq1d 2827 . . . . . . 7 (𝐶 = 𝑋 → ((((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))
173169, 1723anbi23d 1569 . . . . . 6 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)))
174167, 173syl5bbr 277 . . . . 5 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)))
1752, 42, 89syl2anc 581 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ∈ On)
176 oen0 7933 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝑋 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝑋))
1772, 42, 130, 176syl21anc 873 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ∅ ∈ (𝐴o 𝑋))
178177ne0d 4151 . . . . . 6 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (𝐴o 𝑋) ≠ ∅)
179 omeu 7932 . . . . . . 7 (((𝐴o 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴o 𝑋) ≠ ∅) → ∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
180 oeeu.2 . . . . . . . . 9 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵))
181 opeq1 4623 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → ⟨𝑦, 𝑧⟩ = ⟨𝑑, 𝑧⟩)
182181eqeq2d 2835 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → (𝑤 = ⟨𝑦, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑧⟩))
183 oveq2 6913 . . . . . . . . . . . . . . 15 (𝑦 = 𝑑 → ((𝐴o 𝑋) ·o 𝑦) = ((𝐴o 𝑋) ·o 𝑑))
184183oveq1d 6920 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = (((𝐴o 𝑋) ·o 𝑑) +o 𝑧))
185184eqeq1d 2827 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → ((((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵))
186182, 185anbi12d 626 . . . . . . . . . . . 12 (𝑦 = 𝑑 → ((𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵)))
187 opeq2 4624 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → ⟨𝑑, 𝑧⟩ = ⟨𝑑, 𝑒⟩)
188187eqeq2d 2835 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → (𝑤 = ⟨𝑑, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑒⟩))
189 oveq2 6913 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = (((𝐴o 𝑋) ·o 𝑑) +o 𝑒))
190189eqeq1d 2827 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → ((((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
191188, 190anbi12d 626 . . . . . . . . . . . 12 (𝑧 = 𝑒 → ((𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
192186, 191cbvrex2v 3392 . . . . . . . . . . 11 (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
193 eqeq1 2829 . . . . . . . . . . . . 13 (𝑤 = 𝑎 → (𝑤 = ⟨𝑑, 𝑒⟩ ↔ 𝑎 = ⟨𝑑, 𝑒⟩))
194193anbi1d 625 . . . . . . . . . . . 12 (𝑤 = 𝑎 → ((𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ (𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
1951942rexbidv 3267 . . . . . . . . . . 11 (𝑤 = 𝑎 → (∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
196192, 195syl5bb 275 . . . . . . . . . 10 (𝑤 = 𝑎 → (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)))
197196cbviotav 6092 . . . . . . . . 9 (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴o 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵)) = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
198180, 197eqtri 2849 . . . . . . . 8 𝑃 = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴o 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))
199 oeeu.3 . . . . . . . 8 𝑌 = (1st𝑃)
200 oeeu.4 . . . . . . . 8 𝑍 = (2nd𝑃)
201 oveq2 6913 . . . . . . . . . 10 (𝑑 = 𝐷 → ((𝐴o 𝑋) ·o 𝑑) = ((𝐴o 𝑋) ·o 𝐷))
202201oveq1d 6920 . . . . . . . . 9 (𝑑 = 𝐷 → (((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = (((𝐴o 𝑋) ·o 𝐷) +o 𝑒))
203202eqeq1d 2827 . . . . . . . 8 (𝑑 = 𝐷 → ((((𝐴o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵))
204 oveq2 6913 . . . . . . . . 9 (𝑒 = 𝐸 → (((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = (((𝐴o 𝑋) ·o 𝐷) +o 𝐸))
205204eqeq1d 2827 . . . . . . . 8 (𝑒 = 𝐸 → ((((𝐴o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵 ↔ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))
206198, 199, 200, 203, 205opiota 7491 . . . . . . 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 1496 . . . . 5 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴o 𝑋) ∧ (((𝐴o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
209174, 208sylan9bbr 508 . . . 4 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) ∧ 𝐶 = 𝑋) → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
210209pm5.32da 576 . . 3 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → ((𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
211166, 210bitrd 271 . 2 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
212 3an4anass 1135 . 2 (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴o 𝐶)) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴o 𝐶) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))
213 3anass 1122 . 2 ((𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍)))
214211, 212, 2133bitr4g 306 1 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴o 𝐶)) ∧ (((𝐴o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1113   = wceq 1658  wcel 2166  ∃!weu 2639  wne 2999  wrex 3118  {crab 3121  cdif 3795  wss 3798  c0 4144  {csn 4397  cop 4403   cuni 4658   cint 4697  Ord word 5962  Oncon0 5963  suc csuc 5965  cio 6084  cfv 6123  (class class class)co 6905  1st c1st 7426  2nd c2nd 7427  1oc1o 7819  2oc2o 7820   +o coa 7823   ·o comu 7824  o coe 7825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-omul 7831  df-oexp 7832
This theorem is referenced by:  oeeu  7950  cantnflem3  8865  cantnflem4  8866
  Copyright terms: Public domain W3C validator