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

Theorem oeeui 7727
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 7728 gives an explicit expression for the unique solution of the equation, in terms of the solution 𝑃 to omeu 7710.) (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 3765 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → 𝐴 ∈ On)
21adantr 480 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐴 ∈ On)
32ad2antrr 762 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐴 ∈ On)
4 simprl 809 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 ∈ On)
5 oecl 7662 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝑜 𝐶) ∈ On)
63, 4, 5syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ∈ On)
7 om1 7667 . . . . . . . . . . . . . . 15 ((𝐴𝑜 𝐶) ∈ On → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) = (𝐴𝑜 𝐶))
86, 7syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) = (𝐴𝑜 𝐶))
9 df1o2 7617 . . . . . . . . . . . . . . . 16 1𝑜 = {∅}
10 dif1o 7625 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (𝐴 ∖ 1𝑜) ↔ (𝐷𝐴𝐷 ≠ ∅))
1110simprbi 479 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (𝐴 ∖ 1𝑜) → 𝐷 ≠ ∅)
1211ad2antll 765 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷 ≠ ∅)
13 eldifi 3765 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (𝐴 ∖ 1𝑜) → 𝐷𝐴)
1413ad2antll 765 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷𝐴)
15 onelon 5786 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝐷𝐴) → 𝐷 ∈ On)
163, 14, 15syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷 ∈ On)
17 on0eln0 5818 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ On → (∅ ∈ 𝐷𝐷 ≠ ∅))
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (∅ ∈ 𝐷𝐷 ≠ ∅))
1912, 18mpbird 247 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ 𝐷)
2019snssd 4372 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → {∅} ⊆ 𝐷)
219, 20syl5eqss 3682 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 1𝑜𝐷)
22 1on 7612 . . . . . . . . . . . . . . . . 17 1𝑜 ∈ On
2322a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 1𝑜 ∈ On)
24 omwordi 7696 . . . . . . . . . . . . . . . 16 ((1𝑜 ∈ On ∧ 𝐷 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) → (1𝑜𝐷 → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷)))
2523, 16, 6, 24syl3anc 1366 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (1𝑜𝐷 → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷)))
2621, 25mpd 15 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷))
278, 26eqsstr3d 3673 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷))
28 omcl 7661 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐷 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
296, 16, 28syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
30 simplrl 817 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐸 ∈ (𝐴𝑜 𝐶))
31 onelon 5786 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) → 𝐸 ∈ On)
326, 30, 31syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐸 ∈ On)
33 oaword1 7677 . . . . . . . . . . . . . . 15 ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
3429, 32, 33syl2anc 694 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
35 simplrr 818 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)
3634, 35sseqtrd 3674 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵)
3727, 36sstrd 3646 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ⊆ 𝐵)
38 oeeu.1 . . . . . . . . . . . . . . 15 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
3938oeeulem 7726 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝑋 ∈ On ∧ (𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)))
4039simp3d 1095 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
4140ad2antrr 762 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
4239simp1d 1093 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 ∈ On)
4342ad2antrr 762 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋 ∈ On)
44 suceloni 7055 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → suc 𝑋 ∈ On)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝑋 ∈ On)
46 oecl 7662 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝑋 ∈ On) → (𝐴𝑜 suc 𝑋) ∈ On)
473, 45, 46syl2anc 694 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝑋) ∈ On)
48 ontr2 5810 . . . . . . . . . . . . 13 (((𝐴𝑜 𝐶) ∈ On ∧ (𝐴𝑜 suc 𝑋) ∈ On) → (((𝐴𝑜 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
496, 47, 48syl2anc 694 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
5037, 41, 49mp2and 715 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋))
51 simplll 813 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐴 ∈ (On ∖ 2𝑜))
52 oeord 7713 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝐶 ∈ suc 𝑋 ↔ (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
534, 45, 51, 52syl3anc 1366 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶 ∈ suc 𝑋 ↔ (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
5450, 53mpbird 247 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 ∈ suc 𝑋)
55 onsssuc 5851 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑋 ∈ On) → (𝐶𝑋𝐶 ∈ suc 𝑋))
564, 43, 55syl2anc 694 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶𝑋𝐶 ∈ suc 𝑋))
5754, 56mpbird 247 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶𝑋)
5839simp2d 1094 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
5958ad2antrr 762 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ⊆ 𝐵)
60 eloni 5771 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → Ord 𝐴)
613, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → Ord 𝐴)
62 ordsucss 7060 . . . . . . . . . . . . . . . 16 (Ord 𝐴 → (𝐷𝐴 → suc 𝐷𝐴))
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐷𝐴)
64 suceloni 7055 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ On → suc 𝐷 ∈ On)
6516, 64syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐷 ∈ On)
66 dif20el 7630 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → ∅ ∈ 𝐴)
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ 𝐴)
68 oen0 7711 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝐶))
693, 4, 67, 68syl21anc 1365 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ (𝐴𝑜 𝐶))
70 omword 7695 . . . . . . . . . . . . . . . 16 (((suc 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) ∧ ∅ ∈ (𝐴𝑜 𝐶)) → (suc 𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
7165, 3, 6, 69, 70syl31anc 1369 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (suc 𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
7263, 71mpbid 222 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
73 oaord 7672 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On ∧ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On) → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶))))
7432, 6, 29, 73syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶))))
7530, 74mpbid 222 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
7635, 75eqeltrrd 2731 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
77 odi 7704 . . . . . . . . . . . . . . . . 17 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐷 ∈ On ∧ 1𝑜 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)))
786, 16, 23, 77syl3anc 1366 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)))
79 oa1suc 7656 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ On → (𝐷 +𝑜 1𝑜) = suc 𝐷)
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐷 +𝑜 1𝑜) = suc 𝐷)
8180oveq2d 6706 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷))
828oveq2d 6706 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
8378, 81, 823eqtr3d 2693 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
8476, 83eleqtrrd 2733 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷))
8572, 84sseldd 3637 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
86 oesuc 7652 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
873, 4, 86syl2anc 694 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
8885, 87eleqtrrd 2733 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (𝐴𝑜 suc 𝐶))
89 oecl 7662 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴𝑜 𝑋) ∈ On)
903, 43, 89syl2anc 694 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ∈ On)
91 suceloni 7055 . . . . . . . . . . . . . . 15 (𝐶 ∈ On → suc 𝐶 ∈ On)
9291ad2antrl 764 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐶 ∈ On)
93 oecl 7662 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴𝑜 suc 𝐶) ∈ On)
943, 92, 93syl2anc 694 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝐶) ∈ On)
95 ontr2 5810 . . . . . . . . . . . . 13 (((𝐴𝑜 𝑋) ∈ On ∧ (𝐴𝑜 suc 𝐶) ∈ On) → (((𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝐶)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9690, 94, 95syl2anc 694 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝐶)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9759, 88, 96mp2and 715 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶))
98 oeord 7713 . . . . . . . . . . . 12 ((𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝑋 ∈ suc 𝐶 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9943, 92, 51, 98syl3anc 1366 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝑋 ∈ suc 𝐶 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
10097, 99mpbird 247 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋 ∈ suc 𝐶)
101 onsssuc 5851 . . . . . . . . . . 11 ((𝑋 ∈ On ∧ 𝐶 ∈ On) → (𝑋𝐶𝑋 ∈ suc 𝐶))
10243, 4, 101syl2anc 694 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝑋𝐶𝑋 ∈ suc 𝐶))
103100, 102mpbird 247 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋𝐶)
10457, 103eqssd 3653 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 = 𝑋)
105104, 16jca 553 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶 = 𝑋𝐷 ∈ On))
106 simprl 809 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 = 𝑋)
10742ad2antrr 762 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝑋 ∈ On)
108106, 107eqeltrd 2730 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 ∈ On)
1092ad2antrr 762 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐴 ∈ On)
110109, 108, 5syl2anc 694 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) ∈ On)
111 simprr 811 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ On)
112110, 111, 28syl2anc 694 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
113 simplrl 817 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ (𝐴𝑜 𝐶))
114110, 113, 31syl2anc 694 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ On)
115112, 114, 33syl2anc 694 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
116 simplrr 818 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)
117115, 116sseqtrd 3674 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵)
11840ad2antrr 762 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
119 suceq 5828 . . . . . . . . . . . . . . 15 (𝐶 = 𝑋 → suc 𝐶 = suc 𝑋)
120119ad2antrl 764 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → suc 𝐶 = suc 𝑋)
121120oveq2d 6706 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝐶) = (𝐴𝑜 suc 𝑋))
122109, 108, 86syl2anc 694 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
123121, 122eqtr3d 2687 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝑋) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
124118, 123eleqtrd 2732 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
125 omcl 7661 . . . . . . . . . . . . 13 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On)
126110, 109, 125syl2anc 694 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On)
127 ontr2 5810 . . . . . . . . . . . 12 ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On ∧ ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
128112, 126, 127syl2anc 694 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
129117, 124, 128mp2and 715 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
13066adantr 480 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∅ ∈ 𝐴)
131130ad2antrr 762 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ 𝐴)
132109, 108, 131, 68syl21anc 1365 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ (𝐴𝑜 𝐶))
133 omord2 7692 . . . . . . . . . . 11 (((𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) ∧ ∅ ∈ (𝐴𝑜 𝐶)) → (𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
134111, 109, 110, 132, 133syl31anc 1369 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
135129, 134mpbird 247 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷𝐴)
136106oveq2d 6706 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) = (𝐴𝑜 𝑋))
13758ad2antrr 762 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
138136, 137eqsstrd 3672 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) ⊆ 𝐵)
139 eldifi 3765 . . . . . . . . . . . . . 14 (𝐵 ∈ (On ∖ 1𝑜) → 𝐵 ∈ On)
140139adantl 481 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ On)
141140ad2antrr 762 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ On)
142 ontri1 5795 . . . . . . . . . . . 12 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) → ((𝐴𝑜 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝐶)))
143110, 141, 142syl2anc 694 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝐶)))
144138, 143mpbid 222 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ¬ 𝐵 ∈ (𝐴𝑜 𝐶))
145 om0 7642 . . . . . . . . . . . . . . . . 17 ((𝐴𝑜 𝐶) ∈ On → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
146110, 145syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
147146oveq1d 6705 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) = (∅ +𝑜 𝐸))
148 oa0r 7663 . . . . . . . . . . . . . . . 16 (𝐸 ∈ On → (∅ +𝑜 𝐸) = 𝐸)
149114, 148syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (∅ +𝑜 𝐸) = 𝐸)
150147, 149eqtrd 2685 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) = 𝐸)
151150, 113eqeltrd 2730 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶))
152 oveq2 6698 . . . . . . . . . . . . . . 15 (𝐷 = ∅ → ((𝐴𝑜 𝐶) ·𝑜 𝐷) = ((𝐴𝑜 𝐶) ·𝑜 ∅))
153152oveq1d 6705 . . . . . . . . . . . . . 14 (𝐷 = ∅ → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸))
154153eleq1d 2715 . . . . . . . . . . . . 13 (𝐷 = ∅ → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶)))
155151, 154syl5ibrcom 237 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶)))
156116eleq1d 2715 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶) ↔ 𝐵 ∈ (𝐴𝑜 𝐶)))
157155, 156sylibd 229 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → 𝐵 ∈ (𝐴𝑜 𝐶)))
158157necon3bd 2837 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (¬ 𝐵 ∈ (𝐴𝑜 𝐶) → 𝐷 ≠ ∅))
159144, 158mpd 15 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ≠ ∅)
160135, 159, 10sylanbrc 699 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ (𝐴 ∖ 1𝑜))
161108, 160jca 553 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)))
162105, 161impbida 895 . . . . . 6 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ↔ (𝐶 = 𝑋𝐷 ∈ On)))
163162ex 449 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ↔ (𝐶 = 𝑋𝐷 ∈ On))))
164163pm5.32rd 673 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ ((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))))
165 anass 682 . . . 4 (((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))))
166164, 165syl6bb 276 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))))
167 3anass 1059 . . . . . 6 ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
168 oveq2 6698 . . . . . . . 8 (𝐶 = 𝑋 → (𝐴𝑜 𝐶) = (𝐴𝑜 𝑋))
169168eleq2d 2716 . . . . . . 7 (𝐶 = 𝑋 → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ 𝐸 ∈ (𝐴𝑜 𝑋)))
170168oveq1d 6705 . . . . . . . . 9 (𝐶 = 𝑋 → ((𝐴𝑜 𝐶) ·𝑜 𝐷) = ((𝐴𝑜 𝑋) ·𝑜 𝐷))
171170oveq1d 6705 . . . . . . . 8 (𝐶 = 𝑋 → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸))
172171eqeq1d 2653 . . . . . . 7 (𝐶 = 𝑋 → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))
173169, 1723anbi23d 1442 . . . . . 6 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
174167, 173syl5bbr 274 . . . . 5 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
1752, 42, 89syl2anc 694 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ∈ On)
176 oen0 7711 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝑋 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝑋))
1772, 42, 130, 176syl21anc 1365 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∅ ∈ (𝐴𝑜 𝑋))
178 ne0i 3954 . . . . . . 7 (∅ ∈ (𝐴𝑜 𝑋) → (𝐴𝑜 𝑋) ≠ ∅)
179177, 178syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ≠ ∅)
180 omeu 7710 . . . . . . 7 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴𝑜 𝑋) ≠ ∅) → ∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
181 oeeu.2 . . . . . . . . 9 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵))
182 opeq1 4433 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → ⟨𝑦, 𝑧⟩ = ⟨𝑑, 𝑧⟩)
183182eqeq2d 2661 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → (𝑤 = ⟨𝑦, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑧⟩))
184 oveq2 6698 . . . . . . . . . . . . . . 15 (𝑦 = 𝑑 → ((𝐴𝑜 𝑋) ·𝑜 𝑦) = ((𝐴𝑜 𝑋) ·𝑜 𝑑))
185184oveq1d 6705 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧))
186185eqeq1d 2653 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → ((((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵))
187183, 186anbi12d 747 . . . . . . . . . . . 12 (𝑦 = 𝑑 → ((𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵)))
188 opeq2 4434 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → ⟨𝑑, 𝑧⟩ = ⟨𝑑, 𝑒⟩)
189188eqeq2d 2661 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → (𝑤 = ⟨𝑑, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑒⟩))
190 oveq2 6698 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒))
191190eqeq1d 2653 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → ((((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
192189, 191anbi12d 747 . . . . . . . . . . . 12 (𝑧 = 𝑒 → ((𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
193187, 192cbvrex2v 3210 . . . . . . . . . . 11 (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
194 eqeq1 2655 . . . . . . . . . . . . 13 (𝑤 = 𝑎 → (𝑤 = ⟨𝑑, 𝑒⟩ ↔ 𝑎 = ⟨𝑑, 𝑒⟩))
195194anbi1d 741 . . . . . . . . . . . 12 (𝑤 = 𝑎 → ((𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) ↔ (𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
1961952rexbidv 3086 . . . . . . . . . . 11 (𝑤 = 𝑎 → (∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
197193, 196syl5bb 272 . . . . . . . . . 10 (𝑤 = 𝑎 → (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
198197cbviotav 5895 . . . . . . . . 9 (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵)) = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
199181, 198eqtri 2673 . . . . . . . 8 𝑃 = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
200 oeeu.3 . . . . . . . 8 𝑌 = (1st𝑃)
201 oeeu.4 . . . . . . . 8 𝑍 = (2nd𝑃)
202 oveq2 6698 . . . . . . . . . 10 (𝑑 = 𝐷 → ((𝐴𝑜 𝑋) ·𝑜 𝑑) = ((𝐴𝑜 𝑋) ·𝑜 𝐷))
203202oveq1d 6705 . . . . . . . . 9 (𝑑 = 𝐷 → (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒))
204203eqeq1d 2653 . . . . . . . 8 (𝑑 = 𝐷 → ((((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = 𝐵))
205 oveq2 6698 . . . . . . . . 9 (𝑒 = 𝐸 → (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸))
206205eqeq1d 2653 . . . . . . . 8 (𝑒 = 𝐸 → ((((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))
207199, 200, 201, 204, 206opiota 7273 . . . . . . 7 (∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
208180, 207syl 17 . . . . . 6 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴𝑜 𝑋) ≠ ∅) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
209175, 140, 179, 208syl3anc 1366 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
210174, 209sylan9bbr 737 . . . 4 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ 𝐶 = 𝑋) → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
211210pm5.32da 674 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
212166, 211bitrd 268 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
213 3an4anass 1314 . 2 (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜) ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
214 3anass 1059 . 2 ((𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍)))
215212, 213, 2143bitr4g 303 1 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜) ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐶 = 𝑋𝐷 = 𝑌𝐸 = 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  ∃!weu 2498  wne 2823  wrex 2942  {crab 2945  cdif 3604  wss 3607  c0 3948  {csn 4210  cop 4216   cuni 4468   cint 4507  Ord word 5760  Oncon0 5761  suc csuc 5763  cio 5887  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  1𝑜c1o 7598  2𝑜c2o 7599   +𝑜 coa 7602   ·𝑜 comu 7603  𝑜 coe 7604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-oexp 7611
This theorem is referenced by:  oeeu  7728  cantnflem3  8626  cantnflem4  8627
  Copyright terms: Public domain W3C validator