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

Theorem oeeui 7634
Description: The division algorithm for ordinal exponentiation. (This version of oeeu 7635 gives an explicit expression for the unique solution of the equation, in terms of the solution 𝑃 to omeu 7617.) (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 3715 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → 𝐴 ∈ On)
21adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐴 ∈ On)
32ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐴 ∈ On)
4 simprl 793 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 ∈ On)
5 oecl 7569 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝑜 𝐶) ∈ On)
63, 4, 5syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ∈ On)
7 om1 7574 . . . . . . . . . . . . . . 15 ((𝐴𝑜 𝐶) ∈ On → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) = (𝐴𝑜 𝐶))
86, 7syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) = (𝐴𝑜 𝐶))
9 df1o2 7524 . . . . . . . . . . . . . . . 16 1𝑜 = {∅}
10 dif1o 7532 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (𝐴 ∖ 1𝑜) ↔ (𝐷𝐴𝐷 ≠ ∅))
1110simprbi 480 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (𝐴 ∖ 1𝑜) → 𝐷 ≠ ∅)
1211ad2antll 764 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷 ≠ ∅)
13 eldifi 3715 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (𝐴 ∖ 1𝑜) → 𝐷𝐴)
1413ad2antll 764 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷𝐴)
15 onelon 5712 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝐷𝐴) → 𝐷 ∈ On)
163, 14, 15syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐷 ∈ On)
17 on0eln0 5744 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ On → (∅ ∈ 𝐷𝐷 ≠ ∅))
1816, 17syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (∅ ∈ 𝐷𝐷 ≠ ∅))
1912, 18mpbird 247 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ 𝐷)
2019snssd 4314 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → {∅} ⊆ 𝐷)
219, 20syl5eqss 3633 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 1𝑜𝐷)
22 1on 7519 . . . . . . . . . . . . . . . . 17 1𝑜 ∈ On
2322a1i 11 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 1𝑜 ∈ On)
24 omwordi 7603 . . . . . . . . . . . . . . . 16 ((1𝑜 ∈ On ∧ 𝐷 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) → (1𝑜𝐷 → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷)))
2523, 16, 6, 24syl3anc 1323 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (1𝑜𝐷 → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷)))
2621, 25mpd 15 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 1𝑜) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷))
278, 26eqsstr3d 3624 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐷))
28 omcl 7568 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐷 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
296, 16, 28syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
30 simplrl 799 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐸 ∈ (𝐴𝑜 𝐶))
31 onelon 5712 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) → 𝐸 ∈ On)
326, 30, 31syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐸 ∈ On)
33 oaword1 7584 . . . . . . . . . . . . . . 15 ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
3429, 32, 33syl2anc 692 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
35 simplrr 800 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)
3634, 35sseqtrd 3625 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵)
3727, 36sstrd 3597 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ⊆ 𝐵)
38 oeeu.1 . . . . . . . . . . . . . . 15 𝑋 = {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴𝑜 𝑥)}
3938oeeulem 7633 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝑋 ∈ On ∧ (𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)))
4039simp3d 1073 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
4140ad2antrr 761 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
4239simp1d 1071 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝑋 ∈ On)
4342ad2antrr 761 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋 ∈ On)
44 suceloni 6967 . . . . . . . . . . . . . . 15 (𝑋 ∈ On → suc 𝑋 ∈ On)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝑋 ∈ On)
46 oecl 7569 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝑋 ∈ On) → (𝐴𝑜 suc 𝑋) ∈ On)
473, 45, 46syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝑋) ∈ On)
48 ontr2 5736 . . . . . . . . . . . . 13 (((𝐴𝑜 𝐶) ∈ On ∧ (𝐴𝑜 suc 𝑋) ∈ On) → (((𝐴𝑜 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
496, 47, 48syl2anc 692 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝑋)) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
5037, 41, 49mp2and 714 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋))
51 simplll 797 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐴 ∈ (On ∖ 2𝑜))
52 oeord 7620 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝐶 ∈ suc 𝑋 ↔ (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
534, 45, 51, 52syl3anc 1323 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶 ∈ suc 𝑋 ↔ (𝐴𝑜 𝐶) ∈ (𝐴𝑜 suc 𝑋)))
5450, 53mpbird 247 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 ∈ suc 𝑋)
55 onsssuc 5777 . . . . . . . . . . 11 ((𝐶 ∈ On ∧ 𝑋 ∈ On) → (𝐶𝑋𝐶 ∈ suc 𝑋))
564, 43, 55syl2anc 692 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶𝑋𝐶 ∈ suc 𝑋))
5754, 56mpbird 247 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶𝑋)
5839simp2d 1072 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
5958ad2antrr 761 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ⊆ 𝐵)
60 eloni 5697 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ On → Ord 𝐴)
613, 60syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → Ord 𝐴)
62 ordsucss 6972 . . . . . . . . . . . . . . . 16 (Ord 𝐴 → (𝐷𝐴 → suc 𝐷𝐴))
6361, 14, 62sylc 65 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐷𝐴)
64 suceloni 6967 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ On → suc 𝐷 ∈ On)
6516, 64syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐷 ∈ On)
66 dif20el 7537 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (On ∖ 2𝑜) → ∅ ∈ 𝐴)
6751, 66syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ 𝐴)
68 oen0 7618 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝐶))
693, 4, 67, 68syl21anc 1322 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ∅ ∈ (𝐴𝑜 𝐶))
70 omword 7602 . . . . . . . . . . . . . . . 16 (((suc 𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) ∧ ∅ ∈ (𝐴𝑜 𝐶)) → (suc 𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
7165, 3, 6, 69, 70syl31anc 1326 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (suc 𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
7263, 71mpbid 222 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) ⊆ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
73 oaord 7579 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On ∧ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On) → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶))))
7432, 6, 29, 73syl3anc 1323 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶))))
7530, 74mpbid 222 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
7635, 75eqeltrrd 2699 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
77 odi 7611 . . . . . . . . . . . . . . . . 17 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐷 ∈ On ∧ 1𝑜 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)))
786, 16, 23, 77syl3anc 1323 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)))
79 oa1suc 7563 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ On → (𝐷 +𝑜 1𝑜) = suc 𝐷)
8016, 79syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐷 +𝑜 1𝑜) = suc 𝐷)
8180oveq2d 6626 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 (𝐷 +𝑜 1𝑜)) = ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷))
828oveq2d 6626 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 ((𝐴𝑜 𝐶) ·𝑜 1𝑜)) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
8378, 81, 823eqtr3d 2663 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷) = (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 (𝐴𝑜 𝐶)))
8476, 83eleqtrrd 2701 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 suc 𝐷))
8572, 84sseldd 3588 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
86 oesuc 7559 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
873, 4, 86syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
8885, 87eleqtrrd 2701 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐵 ∈ (𝐴𝑜 suc 𝐶))
89 oecl 7569 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴𝑜 𝑋) ∈ On)
903, 43, 89syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ∈ On)
91 suceloni 6967 . . . . . . . . . . . . . . 15 (𝐶 ∈ On → suc 𝐶 ∈ On)
9291ad2antrl 763 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → suc 𝐶 ∈ On)
93 oecl 7569 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴𝑜 suc 𝐶) ∈ On)
943, 92, 93syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 suc 𝐶) ∈ On)
95 ontr2 5736 . . . . . . . . . . . . 13 (((𝐴𝑜 𝑋) ∈ On ∧ (𝐴𝑜 suc 𝐶) ∈ On) → (((𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝐶)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9690, 94, 95syl2anc 692 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (((𝐴𝑜 𝑋) ⊆ 𝐵𝐵 ∈ (𝐴𝑜 suc 𝐶)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9759, 88, 96mp2and 714 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶))
98 oeord 7620 . . . . . . . . . . . 12 ((𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝑋 ∈ suc 𝐶 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
9943, 92, 51, 98syl3anc 1323 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝑋 ∈ suc 𝐶 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 suc 𝐶)))
10097, 99mpbird 247 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋 ∈ suc 𝐶)
101 onsssuc 5777 . . . . . . . . . . 11 ((𝑋 ∈ On ∧ 𝐶 ∈ On) → (𝑋𝐶𝑋 ∈ suc 𝐶))
10243, 4, 101syl2anc 692 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝑋𝐶𝑋 ∈ suc 𝐶))
103100, 102mpbird 247 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝑋𝐶)
10457, 103eqssd 3604 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → 𝐶 = 𝑋)
105104, 16jca 554 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜))) → (𝐶 = 𝑋𝐷 ∈ On))
106 simprl 793 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 = 𝑋)
10742ad2antrr 761 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝑋 ∈ On)
108106, 107eqeltrd 2698 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐶 ∈ On)
1092ad2antrr 761 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐴 ∈ On)
110109, 108, 5syl2anc 692 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) ∈ On)
111 simprr 795 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ On)
112110, 111, 28syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On)
113 simplrl 799 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ (𝐴𝑜 𝐶))
114110, 113, 31syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐸 ∈ On)
115112, 114, 33syl2anc 692 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸))
116 simplrr 800 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)
117115, 116sseqtrd 3625 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵)
11840ad2antrr 761 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ (𝐴𝑜 suc 𝑋))
119 suceq 5754 . . . . . . . . . . . . . . 15 (𝐶 = 𝑋 → suc 𝐶 = suc 𝑋)
120119ad2antrl 763 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → suc 𝐶 = suc 𝑋)
121120oveq2d 6626 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝐶) = (𝐴𝑜 suc 𝑋))
122109, 108, 86syl2anc 692 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝐶) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
123121, 122eqtr3d 2657 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 suc 𝑋) = ((𝐴𝑜 𝐶) ·𝑜 𝐴))
124118, 123eleqtrd 2700 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
125 omcl 7568 . . . . . . . . . . . . 13 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On)
126110, 109, 125syl2anc 692 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On)
127 ontr2 5736 . . . . . . . . . . . 12 ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ On ∧ ((𝐴𝑜 𝐶) ·𝑜 𝐴) ∈ On) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
128112, 126, 127syl2anc 692 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) ⊆ 𝐵𝐵 ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
129117, 124, 128mp2and 714 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴))
13066adantr 481 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∅ ∈ 𝐴)
131130ad2antrr 761 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ 𝐴)
132109, 108, 131, 68syl21anc 1322 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ∅ ∈ (𝐴𝑜 𝐶))
133 omord2 7599 . . . . . . . . . . 11 (((𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 𝐶) ∈ On) ∧ ∅ ∈ (𝐴𝑜 𝐶)) → (𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
134111, 109, 110, 132, 133syl31anc 1326 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷𝐴 ↔ ((𝐴𝑜 𝐶) ·𝑜 𝐷) ∈ ((𝐴𝑜 𝐶) ·𝑜 𝐴)))
135129, 134mpbird 247 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷𝐴)
136106oveq2d 6626 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) = (𝐴𝑜 𝑋))
13758ad2antrr 761 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝑋) ⊆ 𝐵)
138136, 137eqsstrd 3623 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐴𝑜 𝐶) ⊆ 𝐵)
139 eldifi 3715 . . . . . . . . . . . . . 14 (𝐵 ∈ (On ∖ 1𝑜) → 𝐵 ∈ On)
140139adantl 482 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → 𝐵 ∈ On)
141140ad2antrr 761 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐵 ∈ On)
142 ontri1 5721 . . . . . . . . . . . 12 (((𝐴𝑜 𝐶) ∈ On ∧ 𝐵 ∈ On) → ((𝐴𝑜 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝐶)))
143110, 141, 142syl2anc 692 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴𝑜 𝐶)))
144138, 143mpbid 222 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ¬ 𝐵 ∈ (𝐴𝑜 𝐶))
145 om0 7549 . . . . . . . . . . . . . . . . 17 ((𝐴𝑜 𝐶) ∈ On → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
146110, 145syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
147146oveq1d 6625 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) = (∅ +𝑜 𝐸))
148 oa0r 7570 . . . . . . . . . . . . . . . 16 (𝐸 ∈ On → (∅ +𝑜 𝐸) = 𝐸)
149114, 148syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (∅ +𝑜 𝐸) = 𝐸)
150147, 149eqtrd 2655 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) = 𝐸)
151150, 113eqeltrd 2698 . . . . . . . . . . . . 13 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶))
152 oveq2 6618 . . . . . . . . . . . . . . 15 (𝐷 = ∅ → ((𝐴𝑜 𝐶) ·𝑜 𝐷) = ((𝐴𝑜 𝐶) ·𝑜 ∅))
153152oveq1d 6625 . . . . . . . . . . . . . 14 (𝐷 = ∅ → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸))
154153eleq1d 2683 . . . . . . . . . . . . 13 (𝐷 = ∅ → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶) ↔ (((𝐴𝑜 𝐶) ·𝑜 ∅) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶)))
155151, 154syl5ibrcom 237 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶)))
156116eleq1d 2683 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) ∈ (𝐴𝑜 𝐶) ↔ 𝐵 ∈ (𝐴𝑜 𝐶)))
157155, 156sylibd 229 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐷 = ∅ → 𝐵 ∈ (𝐴𝑜 𝐶)))
158157necon3bd 2804 . . . . . . . . . 10 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (¬ 𝐵 ∈ (𝐴𝑜 𝐶) → 𝐷 ≠ ∅))
159144, 158mpd 15 . . . . . . . . 9 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ≠ ∅)
160135, 159, 10sylanbrc 697 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → 𝐷 ∈ (𝐴 ∖ 1𝑜))
161108, 160jca 554 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋𝐷 ∈ On)) → (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)))
162105, 161impbida 876 . . . . . 6 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ↔ (𝐶 = 𝑋𝐷 ∈ On)))
163162ex 450 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ↔ (𝐶 = 𝑋𝐷 ∈ On))))
164163pm5.32rd 671 . . . 4 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ ((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))))
165 anass 680 . . . 4 (((𝐶 = 𝑋𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))))
166164, 165syl6bb 276 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))))
167 3anass 1040 . . . . . 6 ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
168 oveq2 6618 . . . . . . . 8 (𝐶 = 𝑋 → (𝐴𝑜 𝐶) = (𝐴𝑜 𝑋))
169168eleq2d 2684 . . . . . . 7 (𝐶 = 𝑋 → (𝐸 ∈ (𝐴𝑜 𝐶) ↔ 𝐸 ∈ (𝐴𝑜 𝑋)))
170168oveq1d 6625 . . . . . . . . 9 (𝐶 = 𝑋 → ((𝐴𝑜 𝐶) ·𝑜 𝐷) = ((𝐴𝑜 𝑋) ·𝑜 𝐷))
171170oveq1d 6625 . . . . . . . 8 (𝐶 = 𝑋 → (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸))
172171eqeq1d 2623 . . . . . . 7 (𝐶 = 𝑋 → ((((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))
173169, 1723anbi23d 1399 . . . . . 6 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
174167, 173syl5bbr 274 . . . . 5 (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
1752, 42, 89syl2anc 692 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ∈ On)
176 oen0 7618 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝑋 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝑋))
1772, 42, 130, 176syl21anc 1322 . . . . . . 7 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ∅ ∈ (𝐴𝑜 𝑋))
178 ne0i 3902 . . . . . . 7 (∅ ∈ (𝐴𝑜 𝑋) → (𝐴𝑜 𝑋) ≠ ∅)
179177, 178syl 17 . . . . . 6 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (𝐴𝑜 𝑋) ≠ ∅)
180 omeu 7617 . . . . . . 7 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴𝑜 𝑋) ≠ ∅) → ∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
181 oeeu.2 . . . . . . . . 9 𝑃 = (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵))
182 opeq1 4375 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → ⟨𝑦, 𝑧⟩ = ⟨𝑑, 𝑧⟩)
183182eqeq2d 2631 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → (𝑤 = ⟨𝑦, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑧⟩))
184 oveq2 6618 . . . . . . . . . . . . . . 15 (𝑦 = 𝑑 → ((𝐴𝑜 𝑋) ·𝑜 𝑦) = ((𝐴𝑜 𝑋) ·𝑜 𝑑))
185184oveq1d 6625 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 → (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧))
186185eqeq1d 2623 . . . . . . . . . . . . 13 (𝑦 = 𝑑 → ((((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵))
187183, 186anbi12d 746 . . . . . . . . . . . 12 (𝑦 = 𝑑 → ((𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵)))
188 opeq2 4376 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → ⟨𝑑, 𝑧⟩ = ⟨𝑑, 𝑒⟩)
189188eqeq2d 2631 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → (𝑤 = ⟨𝑑, 𝑧⟩ ↔ 𝑤 = ⟨𝑑, 𝑒⟩))
190 oveq2 6618 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 → (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒))
191190eqeq1d 2623 . . . . . . . . . . . . 13 (𝑧 = 𝑒 → ((((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
192189, 191anbi12d 746 . . . . . . . . . . . 12 (𝑧 = 𝑒 → ((𝑤 = ⟨𝑑, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑧) = 𝐵) ↔ (𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
193187, 192cbvrex2v 3171 . . . . . . . . . . 11 (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
194 eqeq1 2625 . . . . . . . . . . . . 13 (𝑤 = 𝑎 → (𝑤 = ⟨𝑑, 𝑒⟩ ↔ 𝑎 = ⟨𝑑, 𝑒⟩))
195194anbi1d 740 . . . . . . . . . . . 12 (𝑤 = 𝑎 → ((𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) ↔ (𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
1961952rexbidv 3051 . . . . . . . . . . 11 (𝑤 = 𝑎 → (∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
197193, 196syl5bb 272 . . . . . . . . . 10 (𝑤 = 𝑎 → (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵)))
198197cbviotav 5821 . . . . . . . . 9 (℩𝑤𝑦 ∈ On ∃𝑧 ∈ (𝐴𝑜 𝑋)(𝑤 = ⟨𝑦, 𝑧⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵)) = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
199181, 198eqtri 2643 . . . . . . . 8 𝑃 = (℩𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵))
200 oeeu.3 . . . . . . . 8 𝑌 = (1st𝑃)
201 oeeu.4 . . . . . . . 8 𝑍 = (2nd𝑃)
202 oveq2 6618 . . . . . . . . . 10 (𝑑 = 𝐷 → ((𝐴𝑜 𝑋) ·𝑜 𝑑) = ((𝐴𝑜 𝑋) ·𝑜 𝐷))
203202oveq1d 6625 . . . . . . . . 9 (𝑑 = 𝐷 → (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒))
204203eqeq1d 2623 . . . . . . . 8 (𝑑 = 𝐷 → ((((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = 𝐵))
205 oveq2 6618 . . . . . . . . 9 (𝑒 = 𝐸 → (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸))
206205eqeq1d 2623 . . . . . . . 8 (𝑒 = 𝐸 → ((((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝑒) = 𝐵 ↔ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))
207199, 200, 201, 204, 206opiota 7181 . . . . . . 7 (∃!𝑎𝑑 ∈ On ∃𝑒 ∈ (𝐴𝑜 𝑋)(𝑎 = ⟨𝑑, 𝑒⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑑) +𝑜 𝑒) = 𝐵) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
208180, 207syl 17 . . . . . 6 (((𝐴𝑜 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴𝑜 𝑋) ≠ ∅) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
209175, 140, 179, 208syl3anc 1323 . . . . 5 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴𝑜 𝑋) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
210174, 209sylan9bbr 736 . . . 4 (((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) ∧ 𝐶 = 𝑋) → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐷 = 𝑌𝐸 = 𝑍)))
211210pm5.32da 672 . . 3 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → ((𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵))) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
212166, 211bitrd 268 . 2 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌𝐸 = 𝑍))))
213 3an4anass 1288 . 2 (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜) ∧ 𝐸 ∈ (𝐴𝑜 𝐶)) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵) ↔ ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1𝑜)) ∧ (𝐸 ∈ (𝐴𝑜 𝐶) ∧ (((𝐴𝑜 𝐶) ·𝑜 𝐷) +𝑜 𝐸) = 𝐵)))
214 3anass 1040 . 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 384  w3a 1036   = wceq 1480  wcel 1987  ∃!weu 2469  wne 2790  wrex 2908  {crab 2911  cdif 3556  wss 3559  c0 3896  {csn 4153  cop 4159   cuni 4407   cint 4445  Ord word 5686  Oncon0 5687  suc csuc 5689  cio 5813  cfv 5852  (class class class)co 6610  1st c1st 7118  2nd c2nd 7119  1𝑜c1o 7505  2𝑜c2o 7506   +𝑜 coa 7509   ·𝑜 comu 7510  𝑜 coe 7511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-omul 7517  df-oexp 7518
This theorem is referenced by:  oeeu  7635  cantnflem3  8540  cantnflem4  8541
  Copyright terms: Public domain W3C validator