This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 onsuc ⊢ ( 𝑋 ∈ 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 onsuc ⊢ ( 𝐷 ∈ 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 onsuc ⊢ ( 𝐶 ∈ 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 bitrid ⊢ ( 𝑤 = 𝑎 → ( ∃ 𝑦 ∈ 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 𝐸 ) = 𝐵 ) ↔ ( 𝐶 = 𝑋 ∧ 𝐷 = 𝑌 ∧ 𝐸 = 𝑍 ) ) )