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	$⊢ \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} Or (\{1_{𝑜}, 2_{𝑜}\} \cup \{\emptyset\})$

Proof

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

Metamath Proof Explorer

Theorem sltsolem1

Proof