Metamath Proof Explorer

Theorem omeulem2

Description: Lemma for omeu : uniqueness part. (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 29-May-2015)

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

Proof

Step Hyp Ref Expression
1 simp3l ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐷 ∈ On )
2 eloni ⊢ ( 𝐷 ∈ On → Ord 𝐷 )
3 ordsucss ⊢ ( Ord 𝐷 → ( 𝐵 ∈ 𝐷 → suc 𝐵 ⊆ 𝐷 ) )
4 1 2 3 3syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( 𝐵 ∈ 𝐷 → suc 𝐵 ⊆ 𝐷 ) )
5 simp2l ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐵 ∈ On )
6 suceloni ⊢ ( 𝐵 ∈ On → suc 𝐵 ∈ On )
7 5 6 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → suc 𝐵 ∈ On )
8 simp1l ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐴 ∈ On )
9 simp1r ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐴 ≠ ∅ )
10 on0eln0 ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
11 8 10 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
12 9 11 mpbird ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ∅ ∈ 𝐴 )
13 omword ⊢ ( ( ( suc 𝐵 ∈ On ∧ 𝐷 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( suc 𝐵 ⊆ 𝐷 ↔ ( 𝐴 ·o suc 𝐵 ) ⊆ ( 𝐴 ·o 𝐷 ) ) )
14 7 1 8 12 13 syl31anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( suc 𝐵 ⊆ 𝐷 ↔ ( 𝐴 ·o suc 𝐵 ) ⊆ ( 𝐴 ·o 𝐷 ) ) )
15 4 14 sylibd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( 𝐵 ∈ 𝐷 → ( 𝐴 ·o suc 𝐵 ) ⊆ ( 𝐴 ·o 𝐷 ) ) )
16 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐴 ·o 𝐷 ) ∈ On )
17 8 1 16 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( 𝐴 ·o 𝐷 ) ∈ On )
18 simp3r ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐸 ∈ 𝐴 )
19 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝐸 ∈ 𝐴 ) → 𝐸 ∈ On )
20 8 18 19 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐸 ∈ On )
21 oaword1 ⊢ ( ( ( 𝐴 ·o 𝐷 ) ∈ On ∧ 𝐸 ∈ On ) → ( 𝐴 ·o 𝐷 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
22 sstr ⊢ ( ( ( 𝐴 ·o suc 𝐵 ) ⊆ ( 𝐴 ·o 𝐷 ) ∧ ( 𝐴 ·o 𝐷 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) → ( 𝐴 ·o suc 𝐵 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
23 22 expcom ⊢ ( ( 𝐴 ·o 𝐷 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) → ( ( 𝐴 ·o suc 𝐵 ) ⊆ ( 𝐴 ·o 𝐷 ) → ( 𝐴 ·o suc 𝐵 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
24 21 23 syl ⊢ ( ( ( 𝐴 ·o 𝐷 ) ∈ On ∧ 𝐸 ∈ On ) → ( ( 𝐴 ·o suc 𝐵 ) ⊆ ( 𝐴 ·o 𝐷 ) → ( 𝐴 ·o suc 𝐵 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
25 17 20 24 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( 𝐴 ·o suc 𝐵 ) ⊆ ( 𝐴 ·o 𝐷 ) → ( 𝐴 ·o suc 𝐵 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
26 15 25 syld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( 𝐵 ∈ 𝐷 → ( 𝐴 ·o suc 𝐵 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
27 simp2r ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐶 ∈ 𝐴 )
28 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ On )
29 8 27 28 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → 𝐶 ∈ On )
30 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
31 8 5 30 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( 𝐴 ·o 𝐵 ) ∈ On )
32 oaord ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ) → ( 𝐶 ∈ 𝐴 ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) ) )
33 32 biimpa ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ) ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
34 29 8 31 27 33 syl31anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
35 omsuc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
36 8 5 35 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
37 34 36 eleqtrrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( 𝐴 ·o suc 𝐵 ) )
38 ssel ⊢ ( ( 𝐴 ·o suc 𝐵 ) ⊆ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( 𝐴 ·o suc 𝐵 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
39 26 37 38 syl6ci ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( 𝐵 ∈ 𝐷 → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
40 simpr ⊢ ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → 𝐶 ∈ 𝐸 )
41 oaord ⊢ ( ( 𝐶 ∈ On ∧ 𝐸 ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ) → ( 𝐶 ∈ 𝐸 ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐸 ) ) )
42 40 41 syl5ib ⊢ ( ( 𝐶 ∈ On ∧ 𝐸 ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ) → ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐸 ) ) )
43 oveq2 ⊢ ( 𝐵 = 𝐷 → ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐷 ) )
44 43 oveq1d ⊢ ( 𝐵 = 𝐷 → ( ( 𝐴 ·o 𝐵 ) +o 𝐸 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
45 44 adantr ⊢ ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐸 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
46 45 eleq2d ⊢ ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → ( ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐵 ) +o 𝐸 ) ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
47 42 46 mpbidi ⊢ ( ( 𝐶 ∈ On ∧ 𝐸 ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ) → ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
48 29 20 31 47 syl3anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )
49 39 48 jaod ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐷 ∈ On ∧ 𝐸 ∈ 𝐴 ) ) → ( ( 𝐵 ∈ 𝐷 ∨ ( 𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸 ) ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) ) )