nocvxminlem

Description: Lemma for nocvxmin . Given two birthday-minimal elements of a convex class of surreals, they are not comparable. (Contributed by Scott Fenton, 30-Jun-2011)

		Ref	Expression
	Assertion	nocvxminlem	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to (((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A])) \to \neg X <_{s} Y)$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = X \to (x <_{s} z \leftrightarrow X <_{s} z)$
2	1	anbi1d	$⊢ x = X \to ((x <_{s} z \land z <_{s} y) \leftrightarrow (X <_{s} z \land z <_{s} y))$
3	2	imbi1d	$⊢ x = X \to (((x <_{s} z \land z <_{s} y) \to z \in A) \leftrightarrow ((X <_{s} z \land z <_{s} y) \to z \in A))$
4	3	ralbidv	$⊢ x = X \to (\forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A) \leftrightarrow \forall z \in No ((X <_{s} z \land z <_{s} y) \to z \in A))$
5		breq2	$⊢ y = Y \to (z <_{s} y \leftrightarrow z <_{s} Y)$
6	5	anbi2d	$⊢ y = Y \to ((X <_{s} z \land z <_{s} y) \leftrightarrow (X <_{s} z \land z <_{s} Y))$
7	6	imbi1d	$⊢ y = Y \to (((X <_{s} z \land z <_{s} y) \to z \in A) \leftrightarrow ((X <_{s} z \land z <_{s} Y) \to z \in A))$
8	7	ralbidv	$⊢ y = Y \to (\forall z \in No ((X <_{s} z \land z <_{s} y) \to z \in A) \leftrightarrow \forall z \in No ((X <_{s} z \land z <_{s} Y) \to z \in A))$
9	4 8	rspc2v	$⊢ (X \in A \land Y \in A) \to (\forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A) \to \forall z \in No ((X <_{s} z \land z <_{s} Y) \to z \in A))$
10		breq2	$⊢ z = w \to (X <_{s} z \leftrightarrow X <_{s} w)$
11		breq1	$⊢ z = w \to (z <_{s} Y \leftrightarrow w <_{s} Y)$
12	10 11	anbi12d	$⊢ z = w \to ((X <_{s} z \land z <_{s} Y) \leftrightarrow (X <_{s} w \land w <_{s} Y))$
13		eleq1w	$⊢ z = w \to (z \in A \leftrightarrow w \in A)$
14	12 13	imbi12d	$⊢ z = w \to (((X <_{s} z \land z <_{s} Y) \to z \in A) \leftrightarrow ((X <_{s} w \land w <_{s} Y) \to w \in A))$
15	14	rspcv	$⊢ w \in No \to (\forall z \in No ((X <_{s} z \land z <_{s} Y) \to z \in A) \to ((X <_{s} w \land w <_{s} Y) \to w \in A))$
16		bdaydm	$⊢ dom bday = No$
17	16	sseq2i	$⊢ A \subseteq dom bday \leftrightarrow A \subseteq No$
18		bdayfun	$⊢ Fun bday$
19		funfvima2	$⊢ (Fun bday \land A \subseteq dom bday) \to (w \in A \to bday (w) \in bday [A])$
20	18 19	mpan	$⊢ A \subseteq dom bday \to (w \in A \to bday (w) \in bday [A])$
21	17 20	sylbir	$⊢ A \subseteq No \to (w \in A \to bday (w) \in bday [A])$
22	21	imp	$⊢ (A \subseteq No \land w \in A) \to bday (w) \in bday [A]$
23		intss1	$⊢ bday (w) \in bday [A] \to ⋂ bday [A] \subseteq bday (w)$
24	22 23	syl	$⊢ (A \subseteq No \land w \in A) \to ⋂ bday [A] \subseteq bday (w)$
25		imassrn	$⊢ bday [A] \subseteq ran bday$
26		bdayrn	$⊢ ran bday = On$
27	25 26	sseqtri	$⊢ bday [A] \subseteq On$
28	22	ne0d	$⊢ (A \subseteq No \land w \in A) \to bday [A] \neq \emptyset$
29		oninton	$⊢ (bday [A] \subseteq On \land bday [A] \neq \emptyset) \to ⋂ bday [A] \in On$
30	27 28 29	sylancr	$⊢ (A \subseteq No \land w \in A) \to ⋂ bday [A] \in On$
31		bdayelon	$⊢ bday (w) \in On$
32		ontri1	$⊢ (⋂ bday [A] \in On \land bday (w) \in On) \to (⋂ bday [A] \subseteq bday (w) \leftrightarrow \neg bday (w) \in ⋂ bday [A])$
33	30 31 32	sylancl	$⊢ (A \subseteq No \land w \in A) \to (⋂ bday [A] \subseteq bday (w) \leftrightarrow \neg bday (w) \in ⋂ bday [A])$
34	24 33	mpbid	$⊢ (A \subseteq No \land w \in A) \to \neg bday (w) \in ⋂ bday [A]$
35	34	ex	$⊢ A \subseteq No \to (w \in A \to \neg bday (w) \in ⋂ bday [A])$
36		eleq2	$⊢ bday (X) = ⋂ bday [A] \to (bday (w) \in bday (X) \leftrightarrow bday (w) \in ⋂ bday [A])$
37	36	notbid	$⊢ bday (X) = ⋂ bday [A] \to (\neg bday (w) \in bday (X) \leftrightarrow \neg bday (w) \in ⋂ bday [A])$
38	37	biimprcd	$⊢ \neg bday (w) \in ⋂ bday [A] \to (bday (X) = ⋂ bday [A] \to \neg bday (w) \in bday (X))$
39	35 38	syl6	$⊢ A \subseteq No \to (w \in A \to (bday (X) = ⋂ bday [A] \to \neg bday (w) \in bday (X)))$
40	39	com3l	$⊢ w \in A \to (bday (X) = ⋂ bday [A] \to (A \subseteq No \to \neg bday (w) \in bday (X)))$
41	40	adantrd	$⊢ w \in A \to ((bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to (A \subseteq No \to \neg bday (w) \in bday (X)))$
42	15 41	syl8	$⊢ w \in No \to (\forall z \in No ((X <_{s} z \land z <_{s} Y) \to z \in A) \to ((X <_{s} w \land w <_{s} Y) \to ((bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to (A \subseteq No \to \neg bday (w) \in bday (X)))))$
43	42	com35	$⊢ w \in No \to (\forall z \in No ((X <_{s} z \land z <_{s} Y) \to z \in A) \to (A \subseteq No \to ((bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to ((X <_{s} w \land w <_{s} Y) \to \neg bday (w) \in bday (X)))))$
44	43	com4l	$⊢ \forall z \in No ((X <_{s} z \land z <_{s} Y) \to z \in A) \to (A \subseteq No \to ((bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to (w \in No \to ((X <_{s} w \land w <_{s} Y) \to \neg bday (w) \in bday (X)))))$
45	9 44	syl6	$⊢ (X \in A \land Y \in A) \to (\forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A) \to (A \subseteq No \to ((bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to (w \in No \to ((X <_{s} w \land w <_{s} Y) \to \neg bday (w) \in bday (X))))))$
46	45	com3l	$⊢ \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A) \to (A \subseteq No \to ((X \in A \land Y \in A) \to ((bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to (w \in No \to ((X <_{s} w \land w <_{s} Y) \to \neg bday (w) \in bday (X))))))$
47	46	impcom	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to ((X \in A \land Y \in A) \to ((bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to (w \in No \to ((X <_{s} w \land w <_{s} Y) \to \neg bday (w) \in bday (X)))))$
48	47	imp42	$⊢ (((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \land w \in No) \to ((X <_{s} w \land w <_{s} Y) \to \neg bday (w) \in bday (X))$
49	48	con2d	$⊢ (((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \land w \in No) \to (bday (w) \in bday (X) \to \neg (X <_{s} w \land w <_{s} Y))$
50		3anass	$⊢ (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y) \leftrightarrow (bday (w) \in bday (X) \land (X <_{s} w \land w <_{s} Y))$
51	50	notbii	$⊢ \neg (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y) \leftrightarrow \neg (bday (w) \in bday (X) \land (X <_{s} w \land w <_{s} Y))$
52		imnan	$⊢ (bday (w) \in bday (X) \to \neg (X <_{s} w \land w <_{s} Y)) \leftrightarrow \neg (bday (w) \in bday (X) \land (X <_{s} w \land w <_{s} Y))$
53	51 52	bitr4i	$⊢ \neg (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y) \leftrightarrow (bday (w) \in bday (X) \to \neg (X <_{s} w \land w <_{s} Y))$
54	49 53	sylibr	$⊢ (((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \land w \in No) \to \neg (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y)$
55	54	nrexdv	$⊢ ((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \to \neg \exists w \in No (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y)$
56		ssel	$⊢ A \subseteq No \to (X \in A \to X \in No)$
57		ssel	$⊢ A \subseteq No \to (Y \in A \to Y \in No)$
58	56 57	anim12d	$⊢ A \subseteq No \to ((X \in A \land Y \in A) \to (X \in No \land Y \in No))$
59	58	imp	$⊢ (A \subseteq No \land (X \in A \land Y \in A)) \to (X \in No \land Y \in No)$
60		eqtr3	$⊢ (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]) \to bday (X) = bday (Y)$
61	59 60	anim12i	$⊢ ((A \subseteq No \land (X \in A \land Y \in A)) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A])) \to ((X \in No \land Y \in No) \land bday (X) = bday (Y))$
62	61	anasss	$⊢ (A \subseteq No \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \to ((X \in No \land Y \in No) \land bday (X) = bday (Y))$
63	62	adantlr	$⊢ ((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \to ((X \in No \land Y \in No) \land bday (X) = bday (Y))$
64		nodense	$⊢ ((X \in No \land Y \in No) \land (bday (X) = bday (Y) \land X <_{s} Y)) \to \exists w \in No (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y)$
65	64	anassrs	$⊢ (((X \in No \land Y \in No) \land bday (X) = bday (Y)) \land X <_{s} Y) \to \exists w \in No (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y)$
66	63 65	sylan	$⊢ (((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \land X <_{s} Y) \to \exists w \in No (bday (w) \in bday (X) \land X <_{s} w \land w <_{s} Y)$
67	55 66	mtand	$⊢ ((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A]))) \to \neg X <_{s} Y$
68	67	ex	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to (((X \in A \land Y \in A) \land (bday (X) = ⋂ bday [A] \land bday (Y) = ⋂ bday [A])) \to \neg X <_{s} Y)$

Metamath Proof Explorer

Theorem nocvxminlem

Proof