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 ⊢ A ∈ On ∧ A ≠ ∅ ∧ B ∈ On ∧ C ∈ A ∧ D ∈ On ∧ E ∈ A → B ∈ D ∨ B = D ∧ C ∈ E → A ⋅ 𝑜 B + 𝑜 C ∈ A ⋅ 𝑜 D + 𝑜 E

Proof

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