Metamath Proof Explorer

Theorem omopth2

Description: An ordered pair-like theorem for ordinal multiplication. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion omopth2 ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ↔ ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 simpl2l ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐵 ∈ On )
2 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
3 1 2 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → Ord 𝐵 )
4 simpl3l ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐷 ∈ On )
5 eloni ⊢ ( 𝐷 ∈ On → Ord 𝐷 )
6 4 5 syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → Ord 𝐷 )
7 ordtri3or ⊢ ( ( Ord 𝐵 ∧ Ord 𝐷 ) → ( 𝐵 ∈ 𝐷 ∨ 𝐵 = 𝐷 ∨ 𝐷 ∈ 𝐵 ) )
8 3 6 7 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐵 ∈ 𝐷 ∨ 𝐵 = 𝐷 ∨ 𝐷 ∈ 𝐵 ) )
9 simpr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
10 simpl1l ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐴 ∈ On )
11 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐴 ·o 𝐷 ) ∈ On )
12 10 4 11 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐴 ·o 𝐷 ) ∈ On )
13 simpl3r ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐸 ∈ 𝐴 )
14 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝐸 ∈ 𝐴 ) → 𝐸 ∈ On )
15 10 13 14 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐸 ∈ On )
16 oacl ⊢ ( ( ( 𝐴 ·o 𝐷 ) ∈ On ∧ 𝐸 ∈ On ) → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ On )
17 12 15 16 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ On )
18 eloni ⊢ ( ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ On → Ord ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
19 ordirr ⊢ ( Ord ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) → ¬ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
20 17 18 19 3syl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ¬ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
21 9 20 eqneltrd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ¬ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
22 orc ⊢ ( 𝐵 ∈ 𝐷 → ( 𝐵 ∈ 𝐷 ∨ ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) ) )
23 omeulem2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( 𝐵 ∈ 𝐷 ∨ ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
24 23 adantr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐵 ∈ 𝐷 ∨ ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
25 22 24 syl5 ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐵 ∈ 𝐷 → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
26 21 25 mtod ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ¬ 𝐵 ∈ 𝐷 )
27 26 pm2.21d ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐵 ∈ 𝐷 → 𝐵 = 𝐷 ) )
28 idd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐵 = 𝐷 → 𝐵 = 𝐷 ) )
29 20 9 neleqtrrd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ¬ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) )
30 orc ⊢ ( 𝐷 ∈ 𝐵 → ( 𝐷 ∈ 𝐵 ∨ ( 𝐷 = 𝐵 ∧ 𝐸 ∈ 𝐶 ) ) )
31 simpl1r ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐴 ≠ ∅ )
32 simpl2r ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐶 ∈ 𝐴 )
33 omeulem2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ) → ( ( 𝐷 ∈ 𝐵 ∨ ( 𝐷 = 𝐵 ∧ 𝐸 ∈ 𝐶 ) ) → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
34 10 31 4 13 1 32 33 syl222anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐷 ∈ 𝐵 ∨ ( 𝐷 = 𝐵 ∧ 𝐸 ∈ 𝐶 ) ) → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
35 30 34 syl5 ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐷 ∈ 𝐵 → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
36 29 35 mtod ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ¬ 𝐷 ∈ 𝐵 )
37 36 pm2.21d ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐷 ∈ 𝐵 → 𝐵 = 𝐷 ) )
38 27 28 37 3jaod ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐵 ∈ 𝐷 ∨ 𝐵 = 𝐷 ∨ 𝐷 ∈ 𝐵 ) → 𝐵 = 𝐷 ) )
39 8 38 mpd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐵 = 𝐷 )
40 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ On )
41 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
42 40 41 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ 𝐴 ) → Ord 𝐶 )
43 10 32 42 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → Ord 𝐶 )
44 eloni ⊢ ( 𝐸 ∈ On → Ord 𝐸 )
45 14 44 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐸 ∈ 𝐴 ) → Ord 𝐸 )
46 10 13 45 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → Ord 𝐸 )
47 ordtri3or ⊢ ( ( Ord 𝐶 ∧ Ord 𝐸 ) → ( 𝐶 ∈ 𝐸 ∨ 𝐶 = 𝐸 ∨ 𝐸 ∈ 𝐶 ) )
48 43 46 47 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐶 ∈ 𝐸 ∨ 𝐶 = 𝐸 ∨ 𝐸 ∈ 𝐶 ) )
49 olc ⊢ ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → ( 𝐵 ∈ 𝐷 ∨ ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) ) )
50 49 24 syl5 ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
51 39 50 mpand ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐶 ∈ 𝐸 → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
52 21 51 mtod ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ¬ 𝐶 ∈ 𝐸 )
53 52 pm2.21d ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐶 ∈ 𝐸 → 𝐶 = 𝐸 ) )
54 idd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐶 = 𝐸 → 𝐶 = 𝐸 ) )
55 39 eqcomd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐷 = 𝐵 )
56 olc ⊢ ( ( 𝐷 = 𝐵 ∧ 𝐸 ∈ 𝐶 ) → ( 𝐷 ∈ 𝐵 ∨ ( 𝐷 = 𝐵 ∧ 𝐸 ∈ 𝐶 ) ) )
57 56 34 syl5 ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐷 = 𝐵 ∧ 𝐸 ∈ 𝐶 ) → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
58 55 57 mpand ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐸 ∈ 𝐶 → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
59 29 58 mtod ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ¬ 𝐸 ∈ 𝐶 )
60 59 pm2.21d ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐸 ∈ 𝐶 → 𝐶 = 𝐸 ) )
61 53 54 60 3jaod ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( ( 𝐶 ∈ 𝐸 ∨ 𝐶 = 𝐸 ∨ 𝐸 ∈ 𝐶 ) → 𝐶 = 𝐸 ) )
62 48 61 mpd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → 𝐶 = 𝐸 )
63 39 62 jca ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) )
64 63 ex ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) → ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) ) )
65 oveq2 ⊢ ( 𝐵 = 𝐷 → ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐷 ) )
66 id ⊢ ( 𝐶 = 𝐸 → 𝐶 = 𝐸 )
67 65 66 oveqan12d ⊢ ( ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
68 64 67 impbid1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ↔ ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) ) )