sltlpss

		Ref	Expression
	Assertion	sltlpss	Could not format assertion : No typesetting found for \|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X ~~( _Left ` X ) C. ( _Left ` Y ) ) ) with typecode \|-~~

Proof

Step	Hyp	Ref	Expression
1		oldssno	$⊢ Old (bday (X)) \subseteq No$
2	1	sseli	$⊢ x \in Old (bday (X)) \to x \in No$
3	2	3ad2ant2	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \land x \in Old (bday (X)) \land x <_{s} X) \to x \in No$
4		simp1l1	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \land x \in Old (bday (X)) \land x <_{s} X) \to X \in No$
5		simp1l2	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \land x \in Old (bday (X)) \land x <_{s} X) \to Y \in No$
6		simp3	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \land x \in Old (bday (X)) \land x <_{s} X) \to x <_{s} X$
7		simp1r	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \land x \in Old (bday (X)) \land x <_{s} X) \to X <_{s} Y$
8	3 4 5 6 7	slttrd	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \land x \in Old (bday (X)) \land x <_{s} X) \to x <_{s} Y$
9	8	3exp	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to (x \in Old (bday (X)) \to (x <_{s} X \to x <_{s} Y))$
10	9	imdistand	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to ((x \in Old (bday (X)) \land x <_{s} X) \to (x \in Old (bday (X)) \land x <_{s} Y))$
11		fveq2	$⊢ bday (X) = bday (Y) \to Old (bday (X)) = Old (bday (Y))$
12	11	3ad2ant3	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to Old (bday (X)) = Old (bday (Y))$
13	12	adantr	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to Old (bday (X)) = Old (bday (Y))$
14	13	eleq2d	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to (x \in Old (bday (X)) \leftrightarrow x \in Old (bday (Y)))$
15	14	anbi1d	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to ((x \in Old (bday (X)) \land x <_{s} Y) \leftrightarrow (x \in Old (bday (Y)) \land x <_{s} Y))$
16	10 15	sylibd	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to ((x \in Old (bday (X)) \land x <_{s} X) \to (x \in Old (bday (Y)) \land x <_{s} Y))$
17		leftval	Could not format ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) \| x
18	17	a1i	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) \| x ~~( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) \| x~~~~
19	18	eleq2d	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) \| x ~~( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) \| x~~~~
20		rabid	$⊢ x \in \{x \in Old (bday (X)) \| x <_{s} X\} \leftrightarrow (x \in Old (bday (X)) \land x <_{s} X)$
21	19 20	bitrdi	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x ~~( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x~~~~
22		leftval	Could not format ( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) \| x
23	22	a1i	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) \| x ~~( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) \| x~~~~
24	23	eleq2d	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( x e. ( _Left ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) \| x ~~( x e. ( _Left ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) \| x~~~~
25		rabid	$⊢ x \in \{x \in Old (bday (Y)) \| x <_{s} Y\} \leftrightarrow (x \in Old (bday (Y)) \land x <_{s} Y)$
26	24 25	bitrdi	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( x e. ( _Left ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x ~~( x e. ( _Left ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x~~~~
27	16 21 26	3imtr4d	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( x e. ( _Left ` X ) -> x e. ( _Left ` Y ) ) ) : No typesetting found for \|- ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( x e. ( _Left ` X ) -> x e. ( _Left ` Y ) ) ) with typecode \|-~~
28	27	ssrdv	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` X ) C_ ( _Left ` Y ) ) : No typesetting found for \|- ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` X ) C_ ( _Left ` Y ) ) with typecode \|-~~~~
29		sltirr	$⊢ Y \in No \to \neg Y <_{s} Y$
30	29	3ad2ant2	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to \neg Y <_{s} Y$
31		breq1	$⊢ X = Y \to (X <_{s} Y \leftrightarrow Y <_{s} Y)$
32	31	notbid	$⊢ X = Y \to (\neg X <_{s} Y \leftrightarrow \neg Y <_{s} Y)$
33	30 32	syl5ibrcom	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (X = Y \to \neg X <_{s} Y)$
34	33	con2d	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (X <_{s} Y \to \neg X = Y)$
35	34	imp	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land X <_{s} Y) \to \neg X = Y$
36		simpr	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` X ) = ( _Left ` Y ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` X ) = ( _Left ` Y ) ) with typecode \|-~~~~
37		lruneq	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) ) : No typesetting found for \|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) ) with typecode \|-
38	37	adantr	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) ) : No typesetting found for \|- ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) ) with typecode \|-~~
39	38	adantr	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) ) with typecode \|-~~
40	39 36	difeq12d	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) ) with typecode \|-~~
41		difundir	Could not format ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( ( _Left ` X ) \ ( _Left ` X ) ) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) : No typesetting found for \|- ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( ( _Left ` X ) \ ( _Left ` X ) ) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) with typecode \|-
42		difid	Could not format ( ( _Left ` X ) \ ( _Left ` X ) ) = (/) : No typesetting found for \|- ( ( _Left ` X ) \ ( _Left ` X ) ) = (/) with typecode \|-
43	42	uneq1i	Could not format ( ( ( _Left ` X ) \ ( _Left ` X ) ) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) = ( (/) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) : No typesetting found for \|- ( ( ( _Left ` X ) \ ( _Left ` X ) ) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) = ( (/) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) with typecode \|-
44		0un	Could not format ( (/) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) = ( ( _Right ` X ) \ ( _Left ` X ) ) : No typesetting found for \|- ( (/) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) = ( ( _Right ` X ) \ ( _Left ` X ) ) with typecode \|-
45	41 43 44	3eqtri	Could not format ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( _Right ` X ) \ ( _Left ` X ) ) : No typesetting found for \|- ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( _Right ` X ) \ ( _Left ` X ) ) with typecode \|-
46		incom	Could not format ( ( _Left ` X ) i^i ( _Right ` X ) ) = ( ( _Right ` X ) i^i ( _Left ` X ) ) : No typesetting found for \|- ( ( _Left ` X ) i^i ( _Right ` X ) ) = ( ( _Right ` X ) i^i ( _Left ` X ) ) with typecode \|-
47		lltropt	Could not format ( _Left ` X ) <
48		ssltdisj	Could not format ( ( _Left ` X ) < ~~( ( _Left ` X ) i^i ( _Right ` X ) ) = (/) ) : No typesetting found for \|- ( ( _Left ` X ) < ~~( ( _Left ` X ) i^i ( _Right ` X ) ) = (/) ) with typecode \|-~~~~
49	47 48	mp1i	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Left ` X ) i^i ( _Right ` X ) ) = (/) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` X ) i^i ( _Right ` X ) ) = (/) ) with typecode \|-~~
50	46 49	eqtr3id	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Right ` X ) i^i ( _Left ` X ) ) = (/) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Right ` X ) i^i ( _Left ` X ) ) = (/) ) with typecode \|-~~
51		disjdif2	Could not format ( ( ( _Right ` X ) i^i ( _Left ` X ) ) = (/) -> ( ( _Right ` X ) \ ( _Left ` X ) ) = ( _Right ` X ) ) : No typesetting found for \|- ( ( ( _Right ` X ) i^i ( _Left ` X ) ) = (/) -> ( ( _Right ` X ) \ ( _Left ` X ) ) = ( _Right ` X ) ) with typecode \|-
52	50 51	syl	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Right ` X ) \ ( _Left ` X ) ) = ( _Right ` X ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Right ` X ) \ ( _Left ` X ) ) = ( _Right ` X ) ) with typecode \|-~~
53	45 52	eqtrid	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( _Right ` X ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( _Right ` X ) ) with typecode \|-~~
54		difundir	Could not format ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( ( ( _Left ` Y ) \ ( _Left ` Y ) ) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) : No typesetting found for \|- ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( ( ( _Left ` Y ) \ ( _Left ` Y ) ) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) with typecode \|-
55		difid	Could not format ( ( _Left ` Y ) \ ( _Left ` Y ) ) = (/) : No typesetting found for \|- ( ( _Left ` Y ) \ ( _Left ` Y ) ) = (/) with typecode \|-
56	55	uneq1i	Could not format ( ( ( _Left ` Y ) \ ( _Left ` Y ) ) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) = ( (/) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) : No typesetting found for \|- ( ( ( _Left ` Y ) \ ( _Left ` Y ) ) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) = ( (/) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) with typecode \|-
57		0un	Could not format ( (/) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) = ( ( _Right ` Y ) \ ( _Left ` Y ) ) : No typesetting found for \|- ( (/) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) = ( ( _Right ` Y ) \ ( _Left ` Y ) ) with typecode \|-
58	54 56 57	3eqtri	Could not format ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( ( _Right ` Y ) \ ( _Left ` Y ) ) : No typesetting found for \|- ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( ( _Right ` Y ) \ ( _Left ` Y ) ) with typecode \|-
59		incom	Could not format ( ( _Left ` Y ) i^i ( _Right ` Y ) ) = ( ( _Right ` Y ) i^i ( _Left ` Y ) ) : No typesetting found for \|- ( ( _Left ` Y ) i^i ( _Right ` Y ) ) = ( ( _Right ` Y ) i^i ( _Left ` Y ) ) with typecode \|-
60		lltropt	Could not format ( _Left ` Y ) <
61		ssltdisj	Could not format ( ( _Left ` Y ) < ~~( ( _Left ` Y ) i^i ( _Right ` Y ) ) = (/) ) : No typesetting found for \|- ( ( _Left ` Y ) < ~~( ( _Left ` Y ) i^i ( _Right ` Y ) ) = (/) ) with typecode \|-~~~~
62	60 61	mp1i	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Left ` Y ) i^i ( _Right ` Y ) ) = (/) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` Y ) i^i ( _Right ` Y ) ) = (/) ) with typecode \|-~~
63	59 62	eqtr3id	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Right ` Y ) i^i ( _Left ` Y ) ) = (/) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Right ` Y ) i^i ( _Left ` Y ) ) = (/) ) with typecode \|-~~
64		disjdif2	Could not format ( ( ( _Right ` Y ) i^i ( _Left ` Y ) ) = (/) -> ( ( _Right ` Y ) \ ( _Left ` Y ) ) = ( _Right ` Y ) ) : No typesetting found for \|- ( ( ( _Right ` Y ) i^i ( _Left ` Y ) ) = (/) -> ( ( _Right ` Y ) \ ( _Left ` Y ) ) = ( _Right ` Y ) ) with typecode \|-
65	63 64	syl	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Right ` Y ) \ ( _Left ` Y ) ) = ( _Right ` Y ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Right ` Y ) \ ( _Left ` Y ) ) = ( _Right ` Y ) ) with typecode \|-~~
66	58 65	eqtrid	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( _Right ` Y ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( _Right ` Y ) ) with typecode \|-~~
67	40 53 66	3eqtr3d	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Right ` X ) = ( _Right ` Y ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Right ` X ) = ( _Right ` Y ) ) with typecode \|-~~~~
68	36 67	oveq12d	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ( ( _Left ` X ) \|s ( _Right ` X ) ) = ( ( _Left ` Y ) \|s ( _Right ` Y ) ) ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` X ) \|s ( _Right ` X ) ) = ( ( _Left ` Y ) \|s ( _Right ` Y ) ) ) with typecode \|-~~
69		simpll1	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~X e. No ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~X e. No ) with typecode \|-~~~~
70		lrcut	Could not format ( X e. No -> ( ( _Left ` X ) \|s ( _Right ` X ) ) = X ) : No typesetting found for \|- ( X e. No -> ( ( _Left ` X ) \|s ( _Right ` X ) ) = X ) with typecode \|-
71	69 70	syl	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` X ) \|s ( _Right ` X ) ) = X ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` X ) \|s ( _Right ` X ) ) = X ) with typecode \|-~~~~
72		simpll2	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~Y e. No ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~Y e. No ) with typecode \|-~~~~
73		lrcut	Could not format ( Y e. No -> ( ( _Left ` Y ) \|s ( _Right ` Y ) ) = Y ) : No typesetting found for \|- ( Y e. No -> ( ( _Left ` Y ) \|s ( _Right ` Y ) ) = Y ) with typecode \|-
74	72 73	syl	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` Y ) \|s ( _Right ` Y ) ) = Y ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( ( _Left ` Y ) \|s ( _Right ` Y ) ) = Y ) with typecode \|-~~~~
75	68 71 74	3eqtr3d	Could not format ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~X = Y ) : No typesetting found for \|- ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~X = Y ) with typecode \|-~~~~
76	35 75	mtand	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~-. ( _Left ` X ) = ( _Left ` Y ) ) : No typesetting found for \|- ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~-. ( _Left ` X ) = ( _Left ` Y ) ) with typecode \|-~~~~
77		dfpss2	Could not format ( ( _Left ` X ) C. ( _Left ` Y ) <-> ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` X ) = ( _Left ` Y ) ) ) : No typesetting found for \|- ( ( _Left ` X ) C. ( _Left ` Y ) <-> ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` X ) = ( _Left ` Y ) ) ) with typecode \|-
78	28 76 77	sylanbrc	Could not format ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` X ) C. ( _Left ` Y ) ) : No typesetting found for \|- ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X ~~( _Left ` X ) C. ( _Left ` Y ) ) with typecode \|-~~~~
79	78	ex	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X ~~( _Left ` X ) C. ( _Left ` Y ) ) ) : No typesetting found for \|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X ~~( _Left ` X ) C. ( _Left ` Y ) ) ) with typecode \|-~~~~
80		dfpss3	Could not format ( ( _Left ` X ) C. ( _Left ` Y ) <-> ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` Y ) C_ ( _Left ` X ) ) ) : No typesetting found for \|- ( ( _Left ` X ) C. ( _Left ` Y ) <-> ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` Y ) C_ ( _Left ` X ) ) ) with typecode \|-
81		ssdif0	Could not format ( ( _Left ` Y ) C_ ( _Left ` X ) <-> ( ( _Left ` Y ) \ ( _Left ` X ) ) = (/) ) : No typesetting found for \|- ( ( _Left ` Y ) C_ ( _Left ` X ) <-> ( ( _Left ` Y ) \ ( _Left ` X ) ) = (/) ) with typecode \|-
82	81	necon3bbii	Could not format ( -. ( _Left ` Y ) C_ ( _Left ` X ) <-> ( ( _Left ` Y ) \ ( _Left ` X ) ) =/= (/) ) : No typesetting found for \|- ( -. ( _Left ` Y ) C_ ( _Left ` X ) <-> ( ( _Left ` Y ) \ ( _Left ` X ) ) =/= (/) ) with typecode \|-
83		n0	Could not format ( ( ( _Left ` Y ) \ ( _Left ` X ) ) =/= (/) <-> E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) ) : No typesetting found for \|- ( ( ( _Left ` Y ) \ ( _Left ` X ) ) =/= (/) <-> E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) ) with typecode \|-
84	82 83	bitri	Could not format ( -. ( _Left ` Y ) C_ ( _Left ` X ) <-> E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) ) : No typesetting found for \|- ( -. ( _Left ` Y ) C_ ( _Left ` X ) <-> E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) ) with typecode \|-
85		eldif	Could not format ( x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) <-> ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) ) : No typesetting found for \|- ( x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) <-> ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) ) with typecode \|-
86	22	a1i	Could not format ( Y e. No -> ( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) \| x ~~( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) \| x~~
87	86	eleq2d	Could not format ( Y e. No -> ( x e. ( _Left ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) \| x ~~( x e. ( _Left ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) \| x~~
88	87 25	bitrdi	Could not format ( Y e. No -> ( x e. ( _Left ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x ~~( x e. ( _Left ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x~~
89	17	a1i	Could not format ( X e. No -> ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) \| x ~~( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) \| x~~
90	89	eleq2d	Could not format ( X e. No -> ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) \| x ~~( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) \| x~~
91	90 20	bitrdi	Could not format ( X e. No -> ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x ~~( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x~~
92	91	notbid	Could not format ( X e. No -> ( -. x e. ( _Left ` X ) <-> -. ( x e. ( _Old ` ( bday ` X ) ) /\ x ~~( -. x e. ( _Left ` X ) <-> -. ( x e. ( _Old ` ( bday ` X ) ) /\ x~~
93		ianor	$⊢ \neg (x \in Old (bday (X)) \land x <_{s} X) \leftrightarrow (\neg x \in Old (bday (X)) \lor \neg x <_{s} X)$
94	92 93	bitrdi	Could not format ( X e. No -> ( -. x e. ( _Left ` X ) <-> ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x ~~( -. x e. ( _Left ` X ) <-> ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x~~
95	88 94	bi2anan9r	Could not format ( ( X e. No /\ Y e. No ) -> ( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x ~~( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x~~
96	95	3adant3	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x ~~( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x~~
97		simprl	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to x \in Old (bday (Y))$
98		simpl3	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to bday (X) = bday (Y)$
99	98	fveq2d	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to Old (bday (X)) = Old (bday (Y))$
100	97 99	eleqtrrd	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to x \in Old (bday (X))$
101	100	pm2.24d	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to (\neg x \in Old (bday (X)) \to X <_{s} Y)$
102		simpll1	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \land \neg x <_{s} X) \to X \in No$
103		oldssno	$⊢ Old (bday (Y)) \subseteq No$
104	103 97	sselid	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to x \in No$
105	104	adantr	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \land \neg x <_{s} X) \to x \in No$
106		simpll2	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \land \neg x <_{s} X) \to Y \in No$
107		simpl1	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to X \in No$
108		slenlt	$⊢ (X \in No \land x \in No) \to (X \leq_{s} x \leftrightarrow \neg x <_{s} X)$
109	107 104 108	syl2anc	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to (X \leq_{s} x \leftrightarrow \neg x <_{s} X)$
110	109	biimpar	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \land \neg x <_{s} X) \to X \leq_{s} x$
111		simplrr	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \land \neg x <_{s} X) \to x <_{s} Y$
112	102 105 106 110 111	slelttrd	$⊢ (((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \land \neg x <_{s} X) \to X <_{s} Y$
113	112	ex	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to (\neg x <_{s} X \to X <_{s} Y)$
114	101 113	jaod	$⊢ ((X \in No \land Y \in No \land bday (X) = bday (Y)) \land (x \in Old (bday (Y)) \land x <_{s} Y)) \to ((\neg x \in Old (bday (X)) \lor \neg x <_{s} X) \to X <_{s} Y)$
115	114	expimpd	$⊢ (X \in No \land Y \in No \land bday (X) = bday (Y)) \to (((x \in Old (bday (Y)) \land x <_{s} Y) \land (\neg x \in Old (bday (X)) \lor \neg x <_{s} X)) \to X <_{s} Y)$
116	96 115	sylbid	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) -> X ~~( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) -> X~~
117	85 116	biimtrid	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) -> X ~~( x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) -> X~~
118	117	exlimdv	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) -> X ~~( E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) -> X~~
119	84 118	biimtrid	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( -. ( _Left ` Y ) C_ ( _Left ` X ) -> X ~~( -. ( _Left ` Y ) C_ ( _Left ` X ) -> X~~
120	119	adantld	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` Y ) C_ ( _Left ` X ) ) -> X ~~( ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` Y ) C_ ( _Left ` X ) ) -> X~~
121	80 120	biimtrid	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _Left ` X ) C. ( _Left ` Y ) -> X ~~( ( _Left ` X ) C. ( _Left ` Y ) -> X~~
122	79 121	impbid	Could not format ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X ~~( _Left ` X ) C. ( _Left ` Y ) ) ) : No typesetting found for \|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X ~~( _Left ` X ) C. ( _Left ` Y ) ) ) with typecode \|-~~~~

Metamath Proof Explorer

Theorem sltlpss

Proof