Theorem sltsolem1

Description: Lemma for sltso . The "sign expansion" binary relation totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011)

	Ref	Expression
Assertion	sltsolem1	⊢ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or ( { 1o , 2o } ∪ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2	1	neii	⊢ ¬ 1o = ∅
3		eqtr2	⊢ ( ( 𝑥 = 1o ∧ 𝑥 = ∅ ) → 1o = ∅ )
4	2 3	mto	⊢ ¬ ( 𝑥 = 1o ∧ 𝑥 = ∅ )
5		1on	⊢ 1o ∈ On
6		0elon	⊢ ∅ ∈ On
7		df-2o	⊢ 2o = suc 1o
8		df-1o	⊢ 1o = suc ∅
9	7 8	eqeq12i	⊢ ( 2o = 1o ↔ suc 1o = suc ∅ )
10		suc11	⊢ ( ( 1o ∈ On ∧ ∅ ∈ On ) → ( suc 1o = suc ∅ ↔ 1o = ∅ ) )
11	9 10	bitrid	⊢ ( ( 1o ∈ On ∧ ∅ ∈ On ) → ( 2o = 1o ↔ 1o = ∅ ) )
12	5 6 11	mp2an	⊢ ( 2o = 1o ↔ 1o = ∅ )
13	1 12	nemtbir	⊢ ¬ 2o = 1o
14		eqtr2	⊢ ( ( 𝑥 = 2o ∧ 𝑥 = 1o ) → 2o = 1o )
15	14	ancoms	⊢ ( ( 𝑥 = 1o ∧ 𝑥 = 2o ) → 2o = 1o )
16	13 15	mto	⊢ ¬ ( 𝑥 = 1o ∧ 𝑥 = 2o )
17		nsuceq0	⊢ suc 1o ≠ ∅
18	7	eqeq1i	⊢ ( 2o = ∅ ↔ suc 1o = ∅ )
19	17 18	nemtbir	⊢ ¬ 2o = ∅
20		eqtr2	⊢ ( ( 𝑥 = 2o ∧ 𝑥 = ∅ ) → 2o = ∅ )
21	20	ancoms	⊢ ( ( 𝑥 = ∅ ∧ 𝑥 = 2o ) → 2o = ∅ )
22	19 21	mto	⊢ ¬ ( 𝑥 = ∅ ∧ 𝑥 = 2o )
23	4 16 22	3pm3.2ni	⊢ ¬ ( ( 𝑥 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑥 = 2o ) )
24		vex	⊢ 𝑥 ∈ V
25	24 24	brtp	⊢ ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑥 ↔ ( ( 𝑥 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑥 = 2o ) ) )
26	23 25	mtbir	⊢ ¬ 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑥
27	26	a1i	⊢ ( 𝑥 ∈ { 1o , 2o , ∅ } → ¬ 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑥 )
28		vex	⊢ 𝑦 ∈ V
29	24 28	brtp	⊢ ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑦 ↔ ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) )
30		vex	⊢ 𝑧 ∈ V
31	28 30	brtp	⊢ ( 𝑦 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑧 ↔ ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) )
32		eqtr2	⊢ ( ( 𝑦 = 1o ∧ 𝑦 = ∅ ) → 1o = ∅ )
33	2 32	mto	⊢ ¬ ( 𝑦 = 1o ∧ 𝑦 = ∅ )
34	33	pm2.21i	⊢ ( ( 𝑦 = 1o ∧ 𝑦 = ∅ ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
35	34	ad2ant2rl	⊢ ( ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ∧ ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
36	35	expcom	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) → ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
37	34	ad2ant2rl	⊢ ( ( ( 𝑦 = 1o ∧ 𝑧 = 2o ) ∧ ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
38	37	expcom	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) → ( ( 𝑦 = 1o ∧ 𝑧 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
39		3mix2	⊢ ( ( 𝑥 = 1o ∧ 𝑧 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
40	39	ad2ant2rl	⊢ ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∧ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
41	40	ex	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) → ( ( 𝑦 = ∅ ∧ 𝑧 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
42	36 38 41	3jaod	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) → ( ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
43		eqtr2	⊢ ( ( 𝑦 = 2o ∧ 𝑦 = 1o ) → 2o = 1o )
44	13 43	mto	⊢ ¬ ( 𝑦 = 2o ∧ 𝑦 = 1o )
45	44	pm2.21i	⊢ ( ( 𝑦 = 2o ∧ 𝑦 = 1o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
46	45	ad2ant2lr	⊢ ( ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∧ ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
47	46	ex	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) → ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
48	45	ad2ant2lr	⊢ ( ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∧ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
49	48	ex	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) → ( ( 𝑦 = 1o ∧ 𝑧 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
50		eqtr2	⊢ ( ( 𝑦 = 2o ∧ 𝑦 = ∅ ) → 2o = ∅ )
51	19 50	mto	⊢ ¬ ( 𝑦 = 2o ∧ 𝑦 = ∅ )
52	51	pm2.21i	⊢ ( ( 𝑦 = 2o ∧ 𝑦 = ∅ ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
53	52	ad2ant2lr	⊢ ( ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∧ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
54	53	ex	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) → ( ( 𝑦 = ∅ ∧ 𝑧 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
55	47 49 54	3jaod	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) → ( ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
56	45	ad2ant2lr	⊢ ( ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ∧ ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
57	56	ex	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) → ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
58	45	ad2ant2lr	⊢ ( ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ∧ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
59	58	ex	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) → ( ( 𝑦 = 1o ∧ 𝑧 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
60	52	ad2ant2lr	⊢ ( ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ∧ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
61	60	ex	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) → ( ( 𝑦 = ∅ ∧ 𝑧 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
62	57 59 61	3jaod	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) → ( ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
63	42 55 62	3jaoi	⊢ ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) → ( ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) ) )
64	63	imp	⊢ ( ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∧ ( ( 𝑦 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑧 = 2o ) ) ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
65	29 31 64	syl2anb	⊢ ( ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑦 ∧ 𝑦 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑧 ) → ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
66	24 30	brtp	⊢ ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑧 ↔ ( ( 𝑥 = 1o ∧ 𝑧 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑧 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑧 = 2o ) ) )
67	65 66	sylibr	⊢ ( ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑦 ∧ 𝑦 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑧 ) → 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑧 )
68	67	a1i	⊢ ( ( 𝑥 ∈ { 1o , 2o , ∅ } ∧ 𝑦 ∈ { 1o , 2o , ∅ } ∧ 𝑧 ∈ { 1o , 2o , ∅ } ) → ( ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑦 ∧ 𝑦 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑧 ) → 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑧 ) )
69	24	eltp	⊢ ( 𝑥 ∈ { 1o , 2o , ∅ } ↔ ( 𝑥 = 1o ∨ 𝑥 = 2o ∨ 𝑥 = ∅ ) )
70	28	eltp	⊢ ( 𝑦 ∈ { 1o , 2o , ∅ } ↔ ( 𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅ ) )
71		eqtr3	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 1o ) → 𝑥 = 𝑦 )
72	71	3mix2d	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 1o ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
73	72	ex	⊢ ( 𝑥 = 1o → ( 𝑦 = 1o → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
74		3mix2	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) )
75	74	3mix1d	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = 2o ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
76	75	ex	⊢ ( 𝑥 = 1o → ( 𝑦 = 2o → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
77		3mix1	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) → ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) )
78	77	3mix1d	⊢ ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
79	78	ex	⊢ ( 𝑥 = 1o → ( 𝑦 = ∅ → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
80	73 76 79	3jaod	⊢ ( 𝑥 = 1o → ( ( 𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅ ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
81		3mix2	⊢ ( ( 𝑦 = 1o ∧ 𝑥 = 2o ) → ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) )
82	81	3mix3d	⊢ ( ( 𝑦 = 1o ∧ 𝑥 = 2o ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
83	82	expcom	⊢ ( 𝑥 = 2o → ( 𝑦 = 1o → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
84		eqtr3	⊢ ( ( 𝑥 = 2o ∧ 𝑦 = 2o ) → 𝑥 = 𝑦 )
85	84	3mix2d	⊢ ( ( 𝑥 = 2o ∧ 𝑦 = 2o ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
86	85	ex	⊢ ( 𝑥 = 2o → ( 𝑦 = 2o → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
87		3mix3	⊢ ( ( 𝑦 = ∅ ∧ 𝑥 = 2o ) → ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) )
88	87	3mix3d	⊢ ( ( 𝑦 = ∅ ∧ 𝑥 = 2o ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
89	88	expcom	⊢ ( 𝑥 = 2o → ( 𝑦 = ∅ → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
90	83 86 89	3jaod	⊢ ( 𝑥 = 2o → ( ( 𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅ ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
91		3mix1	⊢ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) → ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) )
92	91	3mix3d	⊢ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
93	92	expcom	⊢ ( 𝑥 = ∅ → ( 𝑦 = 1o → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
94		3mix3	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) → ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) )
95	94	3mix1d	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = 2o ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
96	95	ex	⊢ ( 𝑥 = ∅ → ( 𝑦 = 2o → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
97		eqtr3	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = ∅ ) → 𝑥 = 𝑦 )
98	97	3mix2d	⊢ ( ( 𝑥 = ∅ ∧ 𝑦 = ∅ ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
99	98	ex	⊢ ( 𝑥 = ∅ → ( 𝑦 = ∅ → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
100	93 96 99	3jaod	⊢ ( 𝑥 = ∅ → ( ( 𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅ ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
101	80 90 100	3jaoi	⊢ ( ( 𝑥 = 1o ∨ 𝑥 = 2o ∨ 𝑥 = ∅ ) → ( ( 𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅ ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) ) )
102	101	imp	⊢ ( ( ( 𝑥 = 1o ∨ 𝑥 = 2o ∨ 𝑥 = ∅ ) ∧ ( 𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅ ) ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
103	69 70 102	syl2anb	⊢ ( ( 𝑥 ∈ { 1o , 2o , ∅ } ∧ 𝑦 ∈ { 1o , 2o , ∅ } ) → ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
104		biid	⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
105	28 24	brtp	⊢ ( 𝑦 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑥 ↔ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) )
106	29 104 105	3orbi123i	⊢ ( ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑥 ) ↔ ( ( ( 𝑥 = 1o ∧ 𝑦 = ∅ ) ∨ ( 𝑥 = 1o ∧ 𝑦 = 2o ) ∨ ( 𝑥 = ∅ ∧ 𝑦 = 2o ) ) ∨ 𝑥 = 𝑦 ∨ ( ( 𝑦 = 1o ∧ 𝑥 = ∅ ) ∨ ( 𝑦 = 1o ∧ 𝑥 = 2o ) ∨ ( 𝑦 = ∅ ∧ 𝑥 = 2o ) ) ) )
107	103 106	sylibr	⊢ ( ( 𝑥 ∈ { 1o , 2o , ∅ } ∧ 𝑦 ∈ { 1o , 2o , ∅ } ) → ( 𝑥 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } 𝑥 ) )
108	27 68 107	issoi	⊢ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or { 1o , 2o , ∅ }
109		df-tp	⊢ { 1o , 2o , ∅ } = ( { 1o , 2o } ∪ { ∅ } )
110		soeq2	⊢ ( { 1o , 2o , ∅ } = ( { 1o , 2o } ∪ { ∅ } ) → ( { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or { 1o , 2o , ∅ } ↔ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or ( { 1o , 2o } ∪ { ∅ } ) ) )
111	109 110	ax-mp	⊢ ( { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or { 1o , 2o , ∅ } ↔ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or ( { 1o , 2o } ∪ { ∅ } ) )
112	108 111	mpbi	⊢ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or ( { 1o , 2o } ∪ { ∅ } )