Theorem 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 C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x z e. A ) ) -> ( ( ( X e. A /\ Y e. A ) /\ ( ( bday ` X ) = |^| ( bday " A ) /\ ( bday ` Y ) = |^| ( bday " A ) ) ) -> -. X

Proof

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