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		onsuc	⊢ ( 𝐵 ∈ 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	imbitrid	⊢ ( ( 𝐶 ∈ 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 𝐸 ) ) )