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	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 𝐸 ) = 𝐵 ) ↔ ( 𝐶 = 𝑋 ∧ 𝐷 = 𝑌 ∧ 𝐸 = 𝑍 ) ) )