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

Theorem oeeui 7916
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 7917 gives an explicit expression for the unique solution of the equation, in terms of the solution 𝑃 to omeu 7899.) (Contributed by Mario Carneiro, 25-May-2015.)
Hypotheses
Ref Expression
oeeu.1 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
oeeu.2 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵))
oeeu.3 𝑌 = (1st𝑃)
oeeu.4 𝑍 = (2nd𝑃)
Assertion
Ref Expression
oeeui ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜) ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍)))
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 3928 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → 𝐴 ∈ On)
21adantr 468 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐴 ∈ On)
32ad2antrr 708 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐴 ∈ On)
4 simprl 778 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 ∈ On)
5 oecl 7851 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝑜 𝐶) ∈ On)
63, 4, 5syl2anc 575 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ∈ On)
7 om1 7856 . . . . . . . . . . . . . . 15 ((𝐴𝑜 𝐶) ∈ On → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) = (𝐴𝑜 𝐶))
86, 7syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) = (𝐴𝑜 𝐶))
9 df1o2 7806 . . . . . . . . . . . . . . . 16 1𝑜 = {∅}
10 dif1o 7814 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (𝐴 ∖ 1𝑜) ↔ (𝐷𝐴𝐷 ≠ ∅))
1110simprbi 486 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (𝐴 ∖ 1𝑜) → 𝐷 ≠ ∅)
1211ad2antll 711 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷 ≠ ∅)
13 eldifi 3928 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (𝐴 ∖ 1𝑜) → 𝐷𝐴)
1413ad2antll 711 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷𝐴)
15 onelon 5958 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝐷𝐴) → 𝐷 ∈ On)
163, 14, 15syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷 ∈ On)
17 on0eln0 5990 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ On → (∅ ∈ 𝐷𝐷 ≠ ∅))
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (∅ ∈ 𝐷𝐷 ≠ ∅))
1912, 18mpbird 248 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ 𝐷)
2019snssd 4527 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → {∅} ⊆ 𝐷)
219, 20syl5eqss 3843 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 1𝑜𝐷)
22 1on 7800 . . . . . . . . . . . . . . . . 17 1𝑜 ∈ On
2322a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 1𝑜 ∈ On)
24 omwordi 7885 . . . . . . . . . . . . . . . 16 ((1𝑜 ∈ On ∧ 𝐷 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) → (1𝑜𝐷 → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷)))
2523, 16, 6, 24syl3anc 1483 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (1𝑜𝐷 → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷)))
2621, 25mpd 15 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷))
278, 26eqsstr3d 3834 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷))
28 omcl 7850 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐷 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
296, 16, 28syl2anc 575 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
30 simplrl 786 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐸 ∈ (𝐴𝑜 𝐶))
31 onelon 5958 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) → 𝐸 ∈ On)
326, 30, 31syl2anc 575 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐸 ∈ On)
33 oaword1 7866 . . . . . . . . . . . . . . 15 ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
3429, 32, 33syl2anc 575 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
35 simplrr 787 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)
3634, 35sseqtrd 3835 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵)
3727, 36sstrd 3805 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ⊆ 𝐵)
38 oeeu.1 . . . . . . . . . . . . . . 15 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
3938oeeulem 7915 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝑋 ∈ On ∧ (𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)))
4039simp3d 1167 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
4140ad2antrr 708 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
4239simp1d 1165 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 ∈ On)
4342ad2antrr 708 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋 ∈ On)
44 suceloni 7240 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → suc 𝑋 ∈ On)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝑋 ∈ On)
46 oecl 7851 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝑋 ∈ On) → (𝐴𝑜 suc 𝑋) ∈ On)
473, 45, 46syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝑋) ∈ On)
48 ontr2 5982 . . . . . . . . . . . . 13 (((𝐴𝑜 𝐶) ∈ On ∧ (𝐴𝑜 suc 𝑋) ∈ On) → (((𝐴𝑜 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
496, 47, 48syl2anc 575 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
5037, 41, 49mp2and 682 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋))
51 simplll 782 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐴 ∈ (On ∖ 2𝑜))
52 oeord 7902 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝐶 ∈ suc 𝑋 ↔ (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
534, 45, 51, 52syl3anc 1483 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶 ∈ suc 𝑋 ↔ (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
5450, 53mpbird 248 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 ∈ suc 𝑋)
55 onsssuc 6023 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑋 ∈ On) → (𝐶𝑋𝐶 ∈ suc 𝑋))
564, 43, 55syl2anc 575 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶𝑋𝐶 ∈ suc 𝑋))
5754, 56mpbird 248 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶𝑋)
5839simp2d 1166 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
5958ad2antrr 708 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ⊆ 𝐵)
60 eloni 5943 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → Ord 𝐴)
613, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → Ord 𝐴)
62 ordsucss 7245 . . . . . . . . . . . . . . . 16 (Ord 𝐴 → (𝐷𝐴 → suc 𝐷𝐴))
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐷𝐴)
64 suceloni 7240 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ On → suc 𝐷 ∈ On)
6516, 64syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐷 ∈ On)
66 dif20el 7819 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → ∅ ∈ 𝐴)
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ 𝐴)
68 oen0 7900 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝐶))
693, 4, 67, 68syl21anc 857 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ (𝐴𝑜 𝐶))
70 omword 7884 . . . . . . . . . . . . . . . 16 (((suc 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) ∧ ∅ ∈ (𝐴𝑜 𝐶)) → (suc 𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
7165, 3, 6, 69, 70syl31anc 1485 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (suc 𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
7263, 71mpbid 223 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
73 oaord 7861 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On ∧ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On) → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶))))
7432, 6, 29, 73syl3anc 1483 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶))))
7530, 74mpbid 223 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
7635, 75eqeltrrd 2885 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
77 odi 7893 . . . . . . . . . . . . . . . . 17 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐷 ∈ On ∧ 1𝑜 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)))
786, 16, 23, 77syl3anc 1483 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)))
79 oa1suc 7845 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ On → (𝐷 +𝑜 1𝑜) = suc 𝐷)
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐷 +𝑜 1𝑜) = suc 𝐷)
8180oveq2d 6887 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷))
828oveq2d 6887 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
8378, 81, 823eqtr3d 2847 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
8476, 83eleqtrrd 2887 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷))
8572, 84sseldd 3796 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
86 oesuc 7841 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
873, 4, 86syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
8885, 87eleqtrrd 2887 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (𝐴𝑜 suc 𝐶))
89 oecl 7851 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴𝑜 𝑋) ∈ On)
903, 43, 89syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ∈ On)
91 suceloni 7240 . . . . . . . . . . . . . . 15 (𝐶 ∈ On → suc 𝐶 ∈ On)
9291ad2antrl 710 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐶 ∈ On)
93 oecl 7851 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴𝑜 suc 𝐶) ∈ On)
943, 92, 93syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝐶) ∈ On)
95 ontr2 5982 . . . . . . . . . . . . 13 (((𝐴𝑜 𝑋) ∈ On ∧ (𝐴𝑜 suc 𝐶) ∈ On) → (((𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝐶)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9690, 94, 95syl2anc 575 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝐶)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9759, 88, 96mp2and 682 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶))
98 oeord 7902 . . . . . . . . . . . 12 ((𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝑋 ∈ suc 𝐶 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9943, 92, 51, 98syl3anc 1483 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝑋 ∈ suc 𝐶 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
10097, 99mpbird 248 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋 ∈ suc 𝐶)
101 onsssuc 6023 . . . . . . . . . . 11 ((𝑋 ∈ On ∧ 𝐶 ∈ On) → (𝑋𝐶𝑋 ∈ suc 𝐶))
10243, 4, 101syl2anc 575 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝑋𝐶𝑋 ∈ suc 𝐶))
103100, 102mpbird 248 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋𝐶)
10457, 103eqssd 3812 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 = 𝑋)
105104, 16jca 503 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶 = 𝑋𝐷 ∈ On))
106 simprl 778 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 = 𝑋)
10742ad2antrr 708 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝑋 ∈ On)
108106, 107eqeltrd 2884 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 ∈ On)
1092ad2antrr 708 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐴 ∈ On)
110109, 108, 5syl2anc 575 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) ∈ On)
111 simprr 780 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ On)
112110, 111, 28syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
113 simplrl 786 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ (𝐴𝑜 𝐶))
114110, 113, 31syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ On)
115112, 114, 33syl2anc 575 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
116 simplrr 787 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)
117115, 116sseqtrd 3835 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵)
11840ad2antrr 708 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
119 suceq 6000 . . . . . . . . . . . . . . 15 (𝐶 = 𝑋 → suc 𝐶 = suc 𝑋)
120119ad2antrl 710 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → suc 𝐶 = suc 𝑋)
121120oveq2d 6887 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝐶) = (𝐴𝑜 suc 𝑋))
122109, 108, 86syl2anc 575 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
123121, 122eqtr3d 2841 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝑋) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
124118, 123eleqtrd 2886 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
125 omcl 7850 . . . . . . . . . . . . 13 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On)
126110, 109, 125syl2anc 575 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On)
127 ontr2 5982 . . . . . . . . . . . 12 ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On ∧ ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
128112, 126, 127syl2anc 575 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
129117, 124, 128mp2and 682 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
13066adantr 468 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∅ ∈ 𝐴)
131130ad2antrr 708 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ 𝐴)
132109, 108, 131, 68syl21anc 857 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ (𝐴𝑜 𝐶))
133 omord2 7881 . . . . . . . . . . 11 (((𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) ∧ ∅ ∈ (𝐴𝑜 𝐶)) → (𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
134111, 109, 110, 132, 133syl31anc 1485 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
135129, 134mpbird 248 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷𝐴)
136106oveq2d 6887 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) = (𝐴𝑜 𝑋))
13758ad2antrr 708 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
138136, 137eqsstrd 3833 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) ⊆ 𝐵)
139 eldifi 3928 . . . . . . . . . . . . . 14 (𝐵 ∈ (On ∖ 1𝑜) → 𝐵 ∈ On)
140139adantl 469 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ On)
141140ad2antrr 708 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ On)
142 ontri1 5967 . . . . . . . . . . . 12 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) → ((𝐴𝑜 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝐶)))
143110, 141, 142syl2anc 575 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝐶)))
144138, 143mpbid 223 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ¬ 𝐵 ∈ (𝐴𝑜 𝐶))
145 om0 7831 . . . . . . . . . . . . . . . . 17 ((𝐴𝑜 𝐶) ∈ On → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
146110, 145syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
147146oveq1d 6886 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) = (∅ +𝑜 𝐸))
148 oa0r 7852 . . . . . . . . . . . . . . . 16 (𝐸 ∈ On → (∅ +𝑜 𝐸) = 𝐸)
149114, 148syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (∅ +𝑜 𝐸) = 𝐸)
150147, 149eqtrd 2839 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) = 𝐸)
151150, 113eqeltrd 2884 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶))
152 oveq2 6879 . . . . . . . . . . . . . . 15 (𝐷 = ∅ → ((𝐴𝑜 𝐶) ·𝑜 𝐷) = ((𝐴𝑜 𝐶) ·𝑜 ∅))
153152oveq1d 6886 . . . . . . . . . . . . . 14 (𝐷 = ∅ → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸))
154153eleq1d 2869 . . . . . . . . . . . . 13 (𝐷 = ∅ → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶)))
155151, 154syl5ibrcom 238 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶)))
156116eleq1d 2869 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶) ↔ 𝐵 ∈ (𝐴𝑜 𝐶)))
157155, 156sylibd 230 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → 𝐵 ∈ (𝐴𝑜 𝐶)))
158157necon3bd 2991 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (¬ 𝐵 ∈ (𝐴𝑜 𝐶) → 𝐷 ≠ ∅))
159144, 158mpd 15 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ≠ ∅)
160135, 159, 10sylanbrc 574 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ (𝐴 ∖ 1𝑜))
161108, 160jca 503 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)))
162105, 161impbida 826 . . . . . 6 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ↔ (𝐶 = 𝑋𝐷 ∈ On)))
163162ex 399 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ↔ (𝐶 = 𝑋𝐷 ∈ On))))
164163pm5.32rd 569 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ ((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))))
165 anass 456 . . . 4 (((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))))
166164, 165syl6bb 278 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))))
167 3anass 1109 . . . . . 6 ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
168 oveq2 6879 . . . . . . . 8 (𝐶 = 𝑋 → (𝐴𝑜 𝐶) = (𝐴𝑜 𝑋))
169168eleq2d 2870 . . . . . . 7 (𝐶 = 𝑋 → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ 𝐸 ∈ (𝐴𝑜 𝑋)))
170168oveq1d 6886 . . . . . . . . 9 (𝐶 = 𝑋 → ((𝐴𝑜 𝐶) ·𝑜 𝐷) = ((𝐴𝑜 𝑋) ·𝑜 𝐷))
171170oveq1d 6886 . . . . . . . 8 (𝐶 = 𝑋 → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸))
172171eqeq1d 2807 . . . . . . 7 (𝐶 = 𝑋 → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))
173169, 1723anbi23d 1556 . . . . . 6 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
174167, 173syl5bbr 276 . . . . 5 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
1752, 42, 89syl2anc 575 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ∈ On)
176 oen0 7900 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝑋 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝑋))
1772, 42, 130, 176syl21anc 857 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∅ ∈ (𝐴𝑜 𝑋))
178177ne0d 4120 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ≠ ∅)
179 omeu 7899 . . . . . . 7 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴𝑜 𝑋) ≠ ∅) → ∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
180 oeeu.2 . . . . . . . . 9 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵))
181 opeq1 4591 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → ⟨𝑦, 𝑧⟩ = ⟨𝑑, 𝑧⟩)
182181eqeq2d 2815 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → (𝑤 = ⟨𝑦, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑧⟩))
183 oveq2 6879 . . . . . . . . . . . . . . 15 (𝑦 = 𝑑 → ((𝐴𝑜 𝑋) ·𝑜 𝑦) = ((𝐴𝑜 𝑋) ·𝑜 𝑑))
184183oveq1d 6886 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧))
185184eqeq1d 2807 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → ((((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵))
186182, 185anbi12d 618 . . . . . . . . . . . 12 (𝑦 = 𝑑 → ((𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵)))
187 opeq2 4592 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → ⟨𝑑, 𝑧⟩ = ⟨𝑑, 𝑒⟩)
188187eqeq2d 2815 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → (𝑤 = ⟨𝑑, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑒⟩))
189 oveq2 6879 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒))
190189eqeq1d 2807 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → ((((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
191188, 190anbi12d 618 . . . . . . . . . . . 12 (𝑧 = 𝑒 → ((𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
192186, 191cbvrex2v 3368 . . . . . . . . . . 11 (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
193 eqeq1 2809 . . . . . . . . . . . . 13 (𝑤 = 𝑎 → (𝑤 = ⟨𝑑, 𝑒⟩ ↔ 𝑎 = ⟨𝑑, 𝑒⟩))
194193anbi1d 617 . . . . . . . . . . . 12 (𝑤 = 𝑎 → ((𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) ↔ (𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
1951942rexbidv 3244 . . . . . . . . . . 11 (𝑤 = 𝑎 → (∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
196192, 195syl5bb 274 . . . . . . . . . 10 (𝑤 = 𝑎 → (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
197196cbviotav 6067 . . . . . . . . 9 (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵)) = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
198180, 197eqtri 2827 . . . . . . . 8 𝑃 = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
199 oeeu.3 . . . . . . . 8 𝑌 = (1st𝑃)
200 oeeu.4 . . . . . . . 8 𝑍 = (2nd𝑃)
201 oveq2 6879 . . . . . . . . . 10 (𝑑 = 𝐷 → ((𝐴𝑜 𝑋) ·𝑜 𝑑) = ((𝐴𝑜 𝑋) ·𝑜 𝐷))
202201oveq1d 6886 . . . . . . . . 9 (𝑑 = 𝐷 → (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒))
203202eqeq1d 2807 . . . . . . . 8 (𝑑 = 𝐷 → ((((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = 𝐵))
204 oveq2 6879 . . . . . . . . 9 (𝑒 = 𝐸 → (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸))
205204eqeq1d 2807 . . . . . . . 8 (𝑒 = 𝐸 → ((((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))
206198, 199, 200, 203, 205opiota 7458 . . . . . . 7 (∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
207179, 206syl 17 . . . . . 6 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴𝑜 𝑋) ≠ ∅) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
208175, 140, 178, 207syl3anc 1483 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
209174, 208sylan9bbr 502 . . . 4 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ 𝐶 = 𝑋) → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
210209pm5.32da 570 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
211166, 210bitrd 270 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
212 3an4anass 1122 . 2 (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜) ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
213 3anass 1109 . 2 ((𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍)))
214211, 212, 2133bitr4g 305 1 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜) ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2158  ∃!weu 2632  wne 2977  wrex 3096  {crab 3099  cdif 3763  wss 3766  c0 4113  {csn 4367  cop 4373   cuni 4626   cint 4665  Ord word 5932  Oncon0 5933  suc csuc 5935  cio 6059  cfv 6098  (class class class)co 6871  1st c1st 7393  2nd c2nd 7394  1𝑜c1o 7786  2𝑜c2o 7787   +𝑜 coa 7790   ·𝑜 comu 7791  𝑜 coe 7792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-1st 7395  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-omul 7798  df-oexp 7799
This theorem is referenced by:  oeeu  7917  cantnflem3  8832  cantnflem4  8833
  Copyright terms: Public domain W3C validator