Metamath Proof Explorer


Theorem oeeui

Description: The division algorithm for ordinal exponentiation. (This version of oeeu gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu .) (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses oeeu.1 𝑋 = { 𝑥 ∈ On ∣ 𝐵 ∈ ( 𝐴o 𝑥 ) }
oeeu.2 𝑃 = ( ℩ 𝑤𝑦 ∈ On ∃ 𝑧 ∈ ( 𝐴o 𝑋 ) ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) )
oeeu.3 𝑌 = ( 1st𝑃 )
oeeu.4 𝑍 = ( 2nd𝑃 )
Assertion oeeui ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ∧ 𝐸 ∈ ( 𝐴o 𝐶 ) ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( 𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 oeeu.1 𝑋 = { 𝑥 ∈ On ∣ 𝐵 ∈ ( 𝐴o 𝑥 ) }
2 oeeu.2 𝑃 = ( ℩ 𝑤𝑦 ∈ On ∃ 𝑧 ∈ ( 𝐴o 𝑋 ) ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) )
3 oeeu.3 𝑌 = ( 1st𝑃 )
4 oeeu.4 𝑍 = ( 2nd𝑃 )
5 eldifi ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ On )
6 5 adantr ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → 𝐴 ∈ On )
7 6 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐴 ∈ On )
8 simprl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐶 ∈ On )
9 oecl ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴o 𝐶 ) ∈ On )
10 7 8 9 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o 𝐶 ) ∈ On )
11 om1 ( ( 𝐴o 𝐶 ) ∈ On → ( ( 𝐴o 𝐶 ) ·o 1o ) = ( 𝐴o 𝐶 ) )
12 10 11 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o 1o ) = ( 𝐴o 𝐶 ) )
13 df1o2 1o = { ∅ }
14 dif1o ( 𝐷 ∈ ( 𝐴 ∖ 1o ) ↔ ( 𝐷𝐴𝐷 ≠ ∅ ) )
15 14 simprbi ( 𝐷 ∈ ( 𝐴 ∖ 1o ) → 𝐷 ≠ ∅ )
16 15 ad2antll ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐷 ≠ ∅ )
17 eldifi ( 𝐷 ∈ ( 𝐴 ∖ 1o ) → 𝐷𝐴 )
18 17 ad2antll ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐷𝐴 )
19 onelon ( ( 𝐴 ∈ On ∧ 𝐷𝐴 ) → 𝐷 ∈ On )
20 7 18 19 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐷 ∈ On )
21 on0eln0 ( 𝐷 ∈ On → ( ∅ ∈ 𝐷𝐷 ≠ ∅ ) )
22 20 21 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ∅ ∈ 𝐷𝐷 ≠ ∅ ) )
23 16 22 mpbird ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ∅ ∈ 𝐷 )
24 23 snssd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → { ∅ } ⊆ 𝐷 )
25 13 24 eqsstrid ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 1o𝐷 )
26 1on 1o ∈ On
27 26 a1i ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 1o ∈ On )
28 omwordi ( ( 1o ∈ On ∧ 𝐷 ∈ On ∧ ( 𝐴o 𝐶 ) ∈ On ) → ( 1o𝐷 → ( ( 𝐴o 𝐶 ) ·o 1o ) ⊆ ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ) )
29 27 20 10 28 syl3anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 1o𝐷 → ( ( 𝐴o 𝐶 ) ·o 1o ) ⊆ ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ) )
30 25 29 mpd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o 1o ) ⊆ ( ( 𝐴o 𝐶 ) ·o 𝐷 ) )
31 12 30 eqsstrrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o 𝐶 ) ⊆ ( ( 𝐴o 𝐶 ) ·o 𝐷 ) )
32 omcl ( ( ( 𝐴o 𝐶 ) ∈ On ∧ 𝐷 ∈ On ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ On )
33 10 20 32 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ On )
34 simplrl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐸 ∈ ( 𝐴o 𝐶 ) )
35 onelon ( ( ( 𝐴o 𝐶 ) ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝐶 ) ) → 𝐸 ∈ On )
36 10 34 35 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐸 ∈ On )
37 oaword1 ( ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ On ∧ 𝐸 ∈ On ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ⊆ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) )
38 33 36 37 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ⊆ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) )
39 simplrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 )
40 38 39 sseqtrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ⊆ 𝐵 )
41 31 40 sstrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o 𝐶 ) ⊆ 𝐵 )
42 1 oeeulem ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( 𝑋 ∈ On ∧ ( 𝐴o 𝑋 ) ⊆ 𝐵𝐵 ∈ ( 𝐴o suc 𝑋 ) ) )
43 42 simp3d ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → 𝐵 ∈ ( 𝐴o suc 𝑋 ) )
44 43 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐵 ∈ ( 𝐴o suc 𝑋 ) )
45 42 simp1d ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → 𝑋 ∈ On )
46 45 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝑋 ∈ On )
47 suceloni ( 𝑋 ∈ On → suc 𝑋 ∈ On )
48 46 47 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → suc 𝑋 ∈ On )
49 oecl ( ( 𝐴 ∈ On ∧ suc 𝑋 ∈ On ) → ( 𝐴o suc 𝑋 ) ∈ On )
50 7 48 49 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o suc 𝑋 ) ∈ On )
51 ontr2 ( ( ( 𝐴o 𝐶 ) ∈ On ∧ ( 𝐴o suc 𝑋 ) ∈ On ) → ( ( ( 𝐴o 𝐶 ) ⊆ 𝐵𝐵 ∈ ( 𝐴o suc 𝑋 ) ) → ( 𝐴o 𝐶 ) ∈ ( 𝐴o suc 𝑋 ) ) )
52 10 50 51 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( ( 𝐴o 𝐶 ) ⊆ 𝐵𝐵 ∈ ( 𝐴o suc 𝑋 ) ) → ( 𝐴o 𝐶 ) ∈ ( 𝐴o suc 𝑋 ) ) )
53 41 44 52 mp2and ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o 𝐶 ) ∈ ( 𝐴o suc 𝑋 ) )
54 simplll ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐴 ∈ ( On ∖ 2o ) )
55 oeord ( ( 𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝐶 ∈ suc 𝑋 ↔ ( 𝐴o 𝐶 ) ∈ ( 𝐴o suc 𝑋 ) ) )
56 8 48 54 55 syl3anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐶 ∈ suc 𝑋 ↔ ( 𝐴o 𝐶 ) ∈ ( 𝐴o suc 𝑋 ) ) )
57 53 56 mpbird ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐶 ∈ suc 𝑋 )
58 onsssuc ( ( 𝐶 ∈ On ∧ 𝑋 ∈ On ) → ( 𝐶𝑋𝐶 ∈ suc 𝑋 ) )
59 8 46 58 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐶𝑋𝐶 ∈ suc 𝑋 ) )
60 57 59 mpbird ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐶𝑋 )
61 42 simp2d ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( 𝐴o 𝑋 ) ⊆ 𝐵 )
62 61 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o 𝑋 ) ⊆ 𝐵 )
63 eloni ( 𝐴 ∈ On → Ord 𝐴 )
64 7 63 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → Ord 𝐴 )
65 ordsucss ( Ord 𝐴 → ( 𝐷𝐴 → suc 𝐷𝐴 ) )
66 64 18 65 sylc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → suc 𝐷𝐴 )
67 suceloni ( 𝐷 ∈ On → suc 𝐷 ∈ On )
68 20 67 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → suc 𝐷 ∈ On )
69 dif20el ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ∈ 𝐴 )
70 54 69 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ∅ ∈ 𝐴 )
71 oen0 ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴o 𝐶 ) )
72 7 8 70 71 syl21anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ∅ ∈ ( 𝐴o 𝐶 ) )
73 omword ( ( ( suc 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ ( 𝐴o 𝐶 ) ∈ On ) ∧ ∅ ∈ ( 𝐴o 𝐶 ) ) → ( suc 𝐷𝐴 ↔ ( ( 𝐴o 𝐶 ) ·o suc 𝐷 ) ⊆ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) )
74 68 7 10 72 73 syl31anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( suc 𝐷𝐴 ↔ ( ( 𝐴o 𝐶 ) ·o suc 𝐷 ) ⊆ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) )
75 66 74 mpbid ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o suc 𝐷 ) ⊆ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
76 oaord ( ( 𝐸 ∈ On ∧ ( 𝐴o 𝐶 ) ∈ On ∧ ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ On ) → ( 𝐸 ∈ ( 𝐴o 𝐶 ) ↔ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) ∈ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( 𝐴o 𝐶 ) ) ) )
77 36 10 33 76 syl3anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐸 ∈ ( 𝐴o 𝐶 ) ↔ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) ∈ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( 𝐴o 𝐶 ) ) ) )
78 34 77 mpbid ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) ∈ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( 𝐴o 𝐶 ) ) )
79 39 78 eqeltrrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐵 ∈ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( 𝐴o 𝐶 ) ) )
80 odi ( ( ( 𝐴o 𝐶 ) ∈ On ∧ 𝐷 ∈ On ∧ 1o ∈ On ) → ( ( 𝐴o 𝐶 ) ·o ( 𝐷 +o 1o ) ) = ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( ( 𝐴o 𝐶 ) ·o 1o ) ) )
81 10 20 27 80 syl3anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o ( 𝐷 +o 1o ) ) = ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( ( 𝐴o 𝐶 ) ·o 1o ) ) )
82 oa1suc ( 𝐷 ∈ On → ( 𝐷 +o 1o ) = suc 𝐷 )
83 20 82 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐷 +o 1o ) = suc 𝐷 )
84 83 oveq2d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o ( 𝐷 +o 1o ) ) = ( ( 𝐴o 𝐶 ) ·o suc 𝐷 ) )
85 12 oveq2d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( ( 𝐴o 𝐶 ) ·o 1o ) ) = ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( 𝐴o 𝐶 ) ) )
86 81 84 85 3eqtr3d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( 𝐴o 𝐶 ) ·o suc 𝐷 ) = ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o ( 𝐴o 𝐶 ) ) )
87 79 86 eleqtrrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐵 ∈ ( ( 𝐴o 𝐶 ) ·o suc 𝐷 ) )
88 75 87 sseldd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐵 ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
89 oesuc ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴o suc 𝐶 ) = ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
90 7 8 89 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o suc 𝐶 ) = ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
91 88 90 eleqtrrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐵 ∈ ( 𝐴o suc 𝐶 ) )
92 oecl ( ( 𝐴 ∈ On ∧ 𝑋 ∈ On ) → ( 𝐴o 𝑋 ) ∈ On )
93 7 46 92 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o 𝑋 ) ∈ On )
94 suceloni ( 𝐶 ∈ On → suc 𝐶 ∈ On )
95 94 ad2antrl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → suc 𝐶 ∈ On )
96 oecl ( ( 𝐴 ∈ On ∧ suc 𝐶 ∈ On ) → ( 𝐴o suc 𝐶 ) ∈ On )
97 7 95 96 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o suc 𝐶 ) ∈ On )
98 ontr2 ( ( ( 𝐴o 𝑋 ) ∈ On ∧ ( 𝐴o suc 𝐶 ) ∈ On ) → ( ( ( 𝐴o 𝑋 ) ⊆ 𝐵𝐵 ∈ ( 𝐴o suc 𝐶 ) ) → ( 𝐴o 𝑋 ) ∈ ( 𝐴o suc 𝐶 ) ) )
99 93 97 98 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( ( ( 𝐴o 𝑋 ) ⊆ 𝐵𝐵 ∈ ( 𝐴o suc 𝐶 ) ) → ( 𝐴o 𝑋 ) ∈ ( 𝐴o suc 𝐶 ) ) )
100 62 91 99 mp2and ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐴o 𝑋 ) ∈ ( 𝐴o suc 𝐶 ) )
101 oeord ( ( 𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝑋 ∈ suc 𝐶 ↔ ( 𝐴o 𝑋 ) ∈ ( 𝐴o suc 𝐶 ) ) )
102 46 95 54 101 syl3anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝑋 ∈ suc 𝐶 ↔ ( 𝐴o 𝑋 ) ∈ ( 𝐴o suc 𝐶 ) ) )
103 100 102 mpbird ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝑋 ∈ suc 𝐶 )
104 onsssuc ( ( 𝑋 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑋𝐶𝑋 ∈ suc 𝐶 ) )
105 46 8 104 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝑋𝐶𝑋 ∈ suc 𝐶 ) )
106 103 105 mpbird ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝑋𝐶 )
107 60 106 eqssd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → 𝐶 = 𝑋 )
108 107 20 jca ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ) → ( 𝐶 = 𝑋𝐷 ∈ On ) )
109 simprl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐶 = 𝑋 )
110 45 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝑋 ∈ On )
111 109 110 eqeltrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐶 ∈ On )
112 6 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐴 ∈ On )
113 112 111 9 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐴o 𝐶 ) ∈ On )
114 simprr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐷 ∈ On )
115 113 114 32 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ On )
116 simplrl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐸 ∈ ( 𝐴o 𝐶 ) )
117 113 116 35 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐸 ∈ On )
118 115 117 37 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ⊆ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) )
119 simplrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 )
120 118 119 sseqtrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ⊆ 𝐵 )
121 43 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐵 ∈ ( 𝐴o suc 𝑋 ) )
122 suceq ( 𝐶 = 𝑋 → suc 𝐶 = suc 𝑋 )
123 122 ad2antrl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → suc 𝐶 = suc 𝑋 )
124 123 oveq2d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐴o suc 𝐶 ) = ( 𝐴o suc 𝑋 ) )
125 112 111 89 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐴o suc 𝐶 ) = ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
126 124 125 eqtr3d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐴o suc 𝑋 ) = ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
127 121 126 eleqtrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐵 ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
128 omcl ( ( ( 𝐴o 𝐶 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ∈ On )
129 113 112 128 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ∈ On )
130 ontr2 ( ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ On ∧ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ∈ On ) → ( ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ⊆ 𝐵𝐵 ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) )
131 115 129 130 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ⊆ 𝐵𝐵 ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) )
132 120 127 131 mp2and ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) )
133 69 adantr ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ∅ ∈ 𝐴 )
134 133 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ∅ ∈ 𝐴 )
135 112 111 134 71 syl21anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ∅ ∈ ( 𝐴o 𝐶 ) )
136 omord2 ( ( ( 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ ( 𝐴o 𝐶 ) ∈ On ) ∧ ∅ ∈ ( 𝐴o 𝐶 ) ) → ( 𝐷𝐴 ↔ ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) )
137 114 112 113 135 136 syl31anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐷𝐴 ↔ ( ( 𝐴o 𝐶 ) ·o 𝐷 ) ∈ ( ( 𝐴o 𝐶 ) ·o 𝐴 ) ) )
138 132 137 mpbird ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐷𝐴 )
139 109 oveq2d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐴o 𝐶 ) = ( 𝐴o 𝑋 ) )
140 61 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐴o 𝑋 ) ⊆ 𝐵 )
141 139 140 eqsstrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐴o 𝐶 ) ⊆ 𝐵 )
142 eldifi ( 𝐵 ∈ ( On ∖ 1o ) → 𝐵 ∈ On )
143 142 adantl ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → 𝐵 ∈ On )
144 143 ad2antrr ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐵 ∈ On )
145 ontri1 ( ( ( 𝐴o 𝐶 ) ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴o 𝐶 ) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ( 𝐴o 𝐶 ) ) )
146 113 144 145 syl2anc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( 𝐴o 𝐶 ) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ( 𝐴o 𝐶 ) ) )
147 141 146 mpbid ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ¬ 𝐵 ∈ ( 𝐴o 𝐶 ) )
148 om0 ( ( 𝐴o 𝐶 ) ∈ On → ( ( 𝐴o 𝐶 ) ·o ∅ ) = ∅ )
149 113 148 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( 𝐴o 𝐶 ) ·o ∅ ) = ∅ )
150 149 oveq1d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( ( 𝐴o 𝐶 ) ·o ∅ ) +o 𝐸 ) = ( ∅ +o 𝐸 ) )
151 oa0r ( 𝐸 ∈ On → ( ∅ +o 𝐸 ) = 𝐸 )
152 117 151 syl ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ∅ +o 𝐸 ) = 𝐸 )
153 150 152 eqtrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( ( 𝐴o 𝐶 ) ·o ∅ ) +o 𝐸 ) = 𝐸 )
154 153 116 eqeltrd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( ( 𝐴o 𝐶 ) ·o ∅ ) +o 𝐸 ) ∈ ( 𝐴o 𝐶 ) )
155 oveq2 ( 𝐷 = ∅ → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) = ( ( 𝐴o 𝐶 ) ·o ∅ ) )
156 155 oveq1d ( 𝐷 = ∅ → ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = ( ( ( 𝐴o 𝐶 ) ·o ∅ ) +o 𝐸 ) )
157 156 eleq1d ( 𝐷 = ∅ → ( ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) ∈ ( 𝐴o 𝐶 ) ↔ ( ( ( 𝐴o 𝐶 ) ·o ∅ ) +o 𝐸 ) ∈ ( 𝐴o 𝐶 ) ) )
158 154 157 syl5ibrcom ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐷 = ∅ → ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) ∈ ( 𝐴o 𝐶 ) ) )
159 119 eleq1d ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) ∈ ( 𝐴o 𝐶 ) ↔ 𝐵 ∈ ( 𝐴o 𝐶 ) ) )
160 158 159 sylibd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐷 = ∅ → 𝐵 ∈ ( 𝐴o 𝐶 ) ) )
161 160 necon3bd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( ¬ 𝐵 ∈ ( 𝐴o 𝐶 ) → 𝐷 ≠ ∅ ) )
162 147 161 mpd ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐷 ≠ ∅ )
163 138 162 14 sylanbrc ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → 𝐷 ∈ ( 𝐴 ∖ 1o ) )
164 111 163 jca ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ∧ ( 𝐶 = 𝑋𝐷 ∈ On ) ) → ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) )
165 108 164 impbida ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) → ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ↔ ( 𝐶 = 𝑋𝐷 ∈ On ) ) )
166 165 ex ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) → ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ↔ ( 𝐶 = 𝑋𝐷 ∈ On ) ) ) )
167 166 pm5.32rd ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ↔ ( ( 𝐶 = 𝑋𝐷 ∈ On ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ) )
168 anass ( ( ( 𝐶 = 𝑋𝐷 ∈ On ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ↔ ( 𝐶 = 𝑋 ∧ ( 𝐷 ∈ On ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ) )
169 167 168 bitrdi ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ↔ ( 𝐶 = 𝑋 ∧ ( 𝐷 ∈ On ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ) ) )
170 3anass ( ( 𝐷 ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( 𝐷 ∈ On ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) )
171 oveq2 ( 𝐶 = 𝑋 → ( 𝐴o 𝐶 ) = ( 𝐴o 𝑋 ) )
172 171 eleq2d ( 𝐶 = 𝑋 → ( 𝐸 ∈ ( 𝐴o 𝐶 ) ↔ 𝐸 ∈ ( 𝐴o 𝑋 ) ) )
173 171 oveq1d ( 𝐶 = 𝑋 → ( ( 𝐴o 𝐶 ) ·o 𝐷 ) = ( ( 𝐴o 𝑋 ) ·o 𝐷 ) )
174 173 oveq1d ( 𝐶 = 𝑋 → ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) )
175 174 eqeq1d ( 𝐶 = 𝑋 → ( ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ↔ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) )
176 172 175 3anbi23d ( 𝐶 = 𝑋 → ( ( 𝐷 ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( 𝐷 ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝑋 ) ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) )
177 170 176 bitr3id ( 𝐶 = 𝑋 → ( ( 𝐷 ∈ On ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ↔ ( 𝐷 ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝑋 ) ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) )
178 6 45 92 syl2anc ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( 𝐴o 𝑋 ) ∈ On )
179 oen0 ( ( ( 𝐴 ∈ On ∧ 𝑋 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴o 𝑋 ) )
180 6 45 133 179 syl21anc ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ∅ ∈ ( 𝐴o 𝑋 ) )
181 180 ne0d ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( 𝐴o 𝑋 ) ≠ ∅ )
182 omeu ( ( ( 𝐴o 𝑋 ) ∈ On ∧ 𝐵 ∈ On ∧ ( 𝐴o 𝑋 ) ≠ ∅ ) → ∃! 𝑎𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) )
183 opeq1 ( 𝑦 = 𝑑 → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑑 , 𝑧 ⟩ )
184 183 eqeq2d ( 𝑦 = 𝑑 → ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ↔ 𝑤 = ⟨ 𝑑 , 𝑧 ⟩ ) )
185 oveq2 ( 𝑦 = 𝑑 → ( ( 𝐴o 𝑋 ) ·o 𝑦 ) = ( ( 𝐴o 𝑋 ) ·o 𝑑 ) )
186 185 oveq1d ( 𝑦 = 𝑑 → ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑧 ) )
187 186 eqeq1d ( 𝑦 = 𝑑 → ( ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ↔ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑧 ) = 𝐵 ) )
188 184 187 anbi12d ( 𝑦 = 𝑑 → ( ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ↔ ( 𝑤 = ⟨ 𝑑 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑧 ) = 𝐵 ) ) )
189 opeq2 ( 𝑧 = 𝑒 → ⟨ 𝑑 , 𝑧 ⟩ = ⟨ 𝑑 , 𝑒 ⟩ )
190 189 eqeq2d ( 𝑧 = 𝑒 → ( 𝑤 = ⟨ 𝑑 , 𝑧 ⟩ ↔ 𝑤 = ⟨ 𝑑 , 𝑒 ⟩ ) )
191 oveq2 ( 𝑧 = 𝑒 → ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑧 ) = ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) )
192 191 eqeq1d ( 𝑧 = 𝑒 → ( ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑧 ) = 𝐵 ↔ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) )
193 190 192 anbi12d ( 𝑧 = 𝑒 → ( ( 𝑤 = ⟨ 𝑑 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑧 ) = 𝐵 ) ↔ ( 𝑤 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) ) )
194 188 193 cbvrex2vw ( ∃ 𝑦 ∈ On ∃ 𝑧 ∈ ( 𝐴o 𝑋 ) ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ↔ ∃ 𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑤 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) )
195 eqeq1 ( 𝑤 = 𝑎 → ( 𝑤 = ⟨ 𝑑 , 𝑒 ⟩ ↔ 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ) )
196 195 anbi1d ( 𝑤 = 𝑎 → ( ( 𝑤 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) ↔ ( 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) ) )
197 196 2rexbidv ( 𝑤 = 𝑎 → ( ∃ 𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑤 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) ↔ ∃ 𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) ) )
198 194 197 syl5bb ( 𝑤 = 𝑎 → ( ∃ 𝑦 ∈ On ∃ 𝑧 ∈ ( 𝐴o 𝑋 ) ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ↔ ∃ 𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) ) )
199 198 cbviotavw ( ℩ 𝑤𝑦 ∈ On ∃ 𝑧 ∈ ( 𝐴o 𝑋 ) ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑦 ) +o 𝑧 ) = 𝐵 ) ) = ( ℩ 𝑎𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) )
200 2 199 eqtri 𝑃 = ( ℩ 𝑎𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) )
201 oveq2 ( 𝑑 = 𝐷 → ( ( 𝐴o 𝑋 ) ·o 𝑑 ) = ( ( 𝐴o 𝑋 ) ·o 𝐷 ) )
202 201 oveq1d ( 𝑑 = 𝐷 → ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝑒 ) )
203 202 eqeq1d ( 𝑑 = 𝐷 → ( ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ↔ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝑒 ) = 𝐵 ) )
204 oveq2 ( 𝑒 = 𝐸 → ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝑒 ) = ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) )
205 204 eqeq1d ( 𝑒 = 𝐸 → ( ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝑒 ) = 𝐵 ↔ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) )
206 200 3 4 203 205 opiota ( ∃! 𝑎𝑑 ∈ On ∃ 𝑒 ∈ ( 𝐴o 𝑋 ) ( 𝑎 = ⟨ 𝑑 , 𝑒 ⟩ ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝑑 ) +o 𝑒 ) = 𝐵 ) → ( ( 𝐷 ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝑋 ) ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( 𝐷 = 𝑌𝐸 = 𝑍 ) ) )
207 182 206 syl ( ( ( 𝐴o 𝑋 ) ∈ On ∧ 𝐵 ∈ On ∧ ( 𝐴o 𝑋 ) ≠ ∅ ) → ( ( 𝐷 ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝑋 ) ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( 𝐷 = 𝑌𝐸 = 𝑍 ) ) )
208 178 143 181 207 syl3anc ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( 𝐷 ∈ On ∧ 𝐸 ∈ ( 𝐴o 𝑋 ) ∧ ( ( ( 𝐴o 𝑋 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( 𝐷 = 𝑌𝐸 = 𝑍 ) ) )
209 177 208 sylan9bbr ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) ∧ 𝐶 = 𝑋 ) → ( ( 𝐷 ∈ On ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ↔ ( 𝐷 = 𝑌𝐸 = 𝑍 ) ) )
210 209 pm5.32da ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( 𝐶 = 𝑋 ∧ ( 𝐷 ∈ On ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ) ↔ ( 𝐶 = 𝑋 ∧ ( 𝐷 = 𝑌𝐸 = 𝑍 ) ) ) )
211 169 210 bitrd ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) ↔ ( 𝐶 = 𝑋 ∧ ( 𝐷 = 𝑌𝐸 = 𝑍 ) ) ) )
212 3an4anass ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ∧ 𝐸 ∈ ( 𝐴o 𝐶 ) ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ) ∧ ( 𝐸 ∈ ( 𝐴o 𝐶 ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ) )
213 3anass ( ( 𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍 ) ↔ ( 𝐶 = 𝑋 ∧ ( 𝐷 = 𝑌𝐸 = 𝑍 ) ) )
214 211 212 213 3bitr4g ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ( 𝐴 ∖ 1o ) ∧ 𝐸 ∈ ( 𝐴o 𝐶 ) ) ∧ ( ( ( 𝐴o 𝐶 ) ·o 𝐷 ) +o 𝐸 ) = 𝐵 ) ↔ ( 𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍 ) ) )