Theorem cofcutr

Description: If X is the cut of A and B , then A is cofinal with (LeftX ) and B is coinitial with ( RightX ) . Theorem 2.9 of Gonshor p. 12. (Contributed by Scott Fenton, 25-Sep-2024)

	Ref	Expression
Assertion	cofcutr	Could not format assertion : No typesetting found for |- ( ( A < ( A. x e. ( _Left ` X ) E. y e. A x <_s y /\ A. z e. ( _Right ` X ) E. w e. B w <_s z ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bdayelon	$$⊢\mathrm{bday}\left(A{|}_{s}B\right)\in \mathrm{On}$$
2	1	onssneli	$$⊢\mathrm{bday}\left(A{|}_{s}B\right)\subseteq \mathrm{bday}\left(x\right)\to \neg \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(A{|}_{s}B\right)$$
3		leftssold	Could not format ( _Left ` X ) C_ ( _Old ` ( bday ` X ) ) : No typesetting found for |- ( _Left ` X ) C_ ( _Old ` ( bday ` X ) ) with typecode |-
4	3	a1i	Could not format ( ( A < ( _Left ` X ) C_ ( _Old ` ( bday ` X ) ) ) : No typesetting found for |- ( ( A < ( _Left ` X ) C_ ( _Old ` ( bday ` X ) ) ) with typecode |-
5	4	sselda	Could not format ( ( ( A < x e. ( _Old ` ( bday ` X ) ) ) : No typesetting found for |- ( ( ( A < x e. ( _Old ` ( bday ` X ) ) ) with typecode |-
6		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
7		leftssno	Could not format ( _Left ` X ) C_ No : No typesetting found for |- ( _Left ` X ) C_ No with typecode |-
8	7	a1i	Could not format ( ( A < ( _Left ` X ) C_ No ) : No typesetting found for |- ( ( A < ( _Left ` X ) C_ No ) with typecode |-
9	8	sselda	Could not format ( ( ( A < x e. No ) : No typesetting found for |- ( ( ( A < x e. No ) with typecode |-
10		oldbday	$$⊢\left(\mathrm{bday}\left(X\right)\in \mathrm{On}\wedge x\in \mathrm{No}\right)\to \left(x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\leftrightarrow \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(X\right)\right)$$
11	6 9 10	sylancr	Could not format ( ( ( A < ( x e. ( _Old ` ( bday ` X ) ) <-> ( bday ` x ) e. ( bday ` X ) ) ) : No typesetting found for |- ( ( ( A < ( x e. ( _Old ` ( bday ` X ) ) <-> ( bday ` x ) e. ( bday ` X ) ) ) with typecode |-
12	5 11	mpbid	Could not format ( ( ( A < ( bday ` x ) e. ( bday ` X ) ) : No typesetting found for |- ( ( ( A < ( bday ` x ) e. ( bday ` X ) ) with typecode |-
13		simplr	Could not format ( ( ( A < X = ( A |s B ) ) : No typesetting found for |- ( ( ( A < X = ( A |s B ) ) with typecode |-
14	13	fveq2d	Could not format ( ( ( A < ( bday ` X ) = ( bday ` ( A |s B ) ) ) : No typesetting found for |- ( ( ( A < ( bday ` X ) = ( bday ` ( A |s B ) ) ) with typecode |-
15	12 14	eleqtrd	Could not format ( ( ( A < ( bday ` x ) e. ( bday ` ( A |s B ) ) ) : No typesetting found for |- ( ( ( A < ( bday ` x ) e. ( bday ` ( A |s B ) ) ) with typecode |-
16	2 15	nsyl3	Could not format ( ( ( A < -. ( bday ` ( A |s B ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( ( A < -. ( bday ` ( A |s B ) ) C_ ( bday ` x ) ) with typecode |-
17		scutbday	$$⊢A{\ll }_{s}B\to \mathrm{bday}\left(A{|}_{s}B\right)=\bigcap \mathrm{bday}\left[\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right]$$
18	17	ad3antrrr	Could not format ( ( ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A <
19		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
20		ssrab2	$$⊢\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\subseteq \mathrm{No}$$
21		sneq	$$⊢t=x\to \left\{t\right\}=\left\{x\right\}$$
22	21	breq2d	$$⊢t=x\to \left(A{\ll }_s\left\{t\right\}\leftrightarrow A{\ll }_s\left\{x\right\}\right)$$
23	21	breq1d	$$⊢t=x\to \left(\left\{t\right\}{\ll }_{s}B\leftrightarrow \left\{x\right\}{\ll }_{s}B\right)$$
24	22 23	anbi12d	$$⊢t=x\to \left(\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\leftrightarrow \left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right)$$
25	9	adantr	Could not format ( ( ( ( A < x e. No ) : No typesetting found for |- ( ( ( ( A < x e. No ) with typecode |-
26		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
27	26	a1i	Could not format ( ( ( A < { x } e. _V ) : No typesetting found for |- ( ( ( A < { x } e. _V ) with typecode |-
28		ssltex2	$$⊢A{\ll }_{s}B\to B\in \mathrm{V}$$
29	28	ad2antrr	Could not format ( ( ( A < B e. _V ) : No typesetting found for |- ( ( ( A < B e. _V ) with typecode |-
30	9	snssd	Could not format ( ( ( A < { x } C_ No ) : No typesetting found for |- ( ( ( A < { x } C_ No ) with typecode |-
31		ssltss2	$$⊢A{\ll }_{s}B\to B\subseteq \mathrm{No}$$
32	31	ad2antrr	Could not format ( ( ( A < B C_ No ) : No typesetting found for |- ( ( ( A < B C_ No ) with typecode |-
33	9	adantr	Could not format ( ( ( ( A < x e. No ) : No typesetting found for |- ( ( ( ( A < x e. No ) with typecode |-
34		simpr	$$⊢\left(A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\to X=A{|}_{s}B$$
35		simpl	$$⊢\left(A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\to A{\ll }_{s}B$$
36	35	scutcld	$$⊢\left(A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\to A{|}_{s}B\in \mathrm{No}$$
37	34 36	eqeltrd	$$⊢\left(A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\to X\in \mathrm{No}$$
38	37	ad2antrr	Could not format ( ( ( ( A < X e. No ) : No typesetting found for |- ( ( ( ( A < X e. No ) with typecode |-
39	32	sselda	Could not format ( ( ( ( A < b e. No ) : No typesetting found for |- ( ( ( ( A < b e. No ) with typecode |-
40		leftval	Could not format ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
41	40	a1i	Could not format ( ( A < ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
42	41	eleq2d	Could not format ( ( A < ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
43		rabid	$$⊢x\in \left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|x{<}_{s}X\right\}\leftrightarrow \left(x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge x{<}_{s}X\right)$$
44	42 43	bitrdi	Could not format ( ( A < ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
45	44	simplbda	Could not format ( ( ( A < x x
46	45	adantr	Could not format ( ( ( ( A < x x
47		simpllr	Could not format ( ( ( ( A < X = ( A |s B ) ) : No typesetting found for |- ( ( ( ( A < X = ( A |s B ) ) with typecode |-
48		scutcut	$$⊢A{\ll }_{s}B\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
49	48	ad2antrr	Could not format ( ( ( A < ( ( A |s B ) e. No /\ A < ( ( A |s B ) e. No /\ A <
50	49	simp3d	Could not format ( ( ( A < { ( A |s B ) } < { ( A |s B ) } <
51		ovex	$$⊢A{|}_{s}B\in \mathrm{V}$$
52	51	snid	$$⊢A{|}_{s}B\in \left\{A{|}_{s}B\right\}$$
53		ssltsepc	$$⊢\left(\left\{A{|}_{s}B\right\}{\ll }_{s}B\wedge A{|}_{s}B\in \left\{A{|}_{s}B\right\}\wedge b\in B\right)\to \left(A{|}_{s}B\right){<}_{s}b$$
54	52 53	mp3an2	$$⊢\left(\left\{A{|}_{s}B\right\}{\ll }_{s}B\wedge b\in B\right)\to \left(A{|}_{s}B\right){<}_{s}b$$
55	50 54	sylan	Could not format ( ( ( ( A < ( A |s B ) ( A |s B )
56	47 55	eqbrtrd	Could not format ( ( ( ( A < X X
57	33 38 39 46 56	slttrd	Could not format ( ( ( ( A < x x
58	57	3adant2	Could not format ( ( ( ( A < x x
59		velsn	$$⊢a\in \left\{x\right\}\leftrightarrow a=x$$
60		breq1	$$⊢a=x\to \left(a{<}_{s}b\leftrightarrow x{<}_{s}b\right)$$
61	59 60	sylbi	$$⊢a\in \left\{x\right\}\to \left(a{<}_{s}b\leftrightarrow x{<}_{s}b\right)$$
62	61	3ad2ant2	Could not format ( ( ( ( A < ( a x ( a x
63	58 62	mpbird	Could not format ( ( ( ( A < a a
64	27 29 30 32 63	ssltd	Could not format ( ( ( A < { x } < { x } <
65	64	anim1ci	Could not format ( ( ( ( A < ( A < ( A <
66	24 25 65	elrabd	Could not format ( ( ( ( A < x e. { t e. No | ( A < x e. { t e. No | ( A <
67		fnfvima	$$⊢\left(\mathrm{bday}Fn\mathrm{No}\wedge \left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\subseteq \mathrm{No}\wedge x\in \left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right)\to \mathrm{bday}\left(x\right)\in \mathrm{bday}\left[\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right]$$
68	19 20 66 67	mp3an12i	Could not format ( ( ( ( A < ( bday ` x ) e. ( bday " { t e. No | ( A < ( bday ` x ) e. ( bday " { t e. No | ( A <
69		intss1	$$⊢\mathrm{bday}\left(x\right)\in \mathrm{bday}\left[\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right]\to \bigcap \mathrm{bday}\left[\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right]\subseteq \mathrm{bday}\left(x\right)$$
70	68 69	syl	Could not format ( ( ( ( A < |^| ( bday " { t e. No | ( A < |^| ( bday " { t e. No | ( A <
71	18 70	eqsstrd	Could not format ( ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` x ) ) with typecode |-
72	16 71	mtand	Could not format ( ( ( A < -. A < -. A <
73		ssltex1	$$⊢A{\ll }_{s}B\to A\in \mathrm{V}$$
74	73	ad3antrrr	Could not format ( ( ( ( A < A e. _V ) : No typesetting found for |- ( ( ( ( A < A e. _V ) with typecode |-
75	74 26	jctir	Could not format ( ( ( ( A < ( A e. _V /\ { x } e. _V ) ) : No typesetting found for |- ( ( ( ( A < ( A e. _V /\ { x } e. _V ) ) with typecode |-
76		ssltss1	$$⊢A{\ll }_{s}B\to A\subseteq \mathrm{No}$$
77	76	ad3antrrr	Could not format ( ( ( ( A < A C_ No ) : No typesetting found for |- ( ( ( ( A < A C_ No ) with typecode |-
78	9	adantr	Could not format ( ( ( ( A < x e. No ) : No typesetting found for |- ( ( ( ( A < x e. No ) with typecode |-
79	78	snssd	Could not format ( ( ( ( A < { x } C_ No ) : No typesetting found for |- ( ( ( ( A < { x } C_ No ) with typecode |-
80		simpr	Could not format ( ( ( ( A < A. y e. A A. t e. { x } y A. y e. A A. t e. { x } y
81	77 79 80	3jca	Could not format ( ( ( ( A < ( A C_ No /\ { x } C_ No /\ A. y e. A A. t e. { x } y ( A C_ No /\ { x } C_ No /\ A. y e. A A. t e. { x } y
82		brsslt	$$⊢A{\ll }_s\left\{x\right\}\leftrightarrow \left(\left(A\in \mathrm{V}\wedge \left\{x\right\}\in \mathrm{V}\right)\wedge \left(A\subseteq \mathrm{No}\wedge \left\{x\right\}\subseteq \mathrm{No}\wedge \forall y\in A\forall t\in \left\{x\right\}y{<}_{s}t\right)\right)$$
83	75 81 82	sylanbrc	Could not format ( ( ( ( A < A < A <
84	72 83	mtand	Could not format ( ( ( A < -. A. y e. A A. t e. { x } y -. A. y e. A A. t e. { x } y
85		rexnal	$$⊢\exists t\in \left\{x\right\}\neg \forall y\in Ay{<}_{s}t\leftrightarrow \neg \forall t\in \left\{x\right\}\forall y\in Ay{<}_{s}t$$
86		ralcom	$$⊢\forall t\in \left\{x\right\}\forall y\in Ay{<}_{s}t\leftrightarrow \forall y\in A\forall t\in \left\{x\right\}y{<}_{s}t$$
87	85 86	xchbinx	$$⊢\exists t\in \left\{x\right\}\neg \forall y\in Ay{<}_{s}t\leftrightarrow \neg \forall y\in A\forall t\in \left\{x\right\}y{<}_{s}t$$
88	84 87	sylibr	Could not format ( ( ( A < E. t e. { x } -. A. y e. A y E. t e. { x } -. A. y e. A y
89		vex	$$⊢x\in \mathrm{V}$$
90		breq2	$$⊢t=x\to \left(y{<}_{s}t\leftrightarrow y{<}_{s}x\right)$$
91	90	ralbidv	$$⊢t=x\to \left(\forall y\in Ay{<}_{s}t\leftrightarrow \forall y\in Ay{<}_{s}x\right)$$
92	91	notbid	$$⊢t=x\to \left(\neg \forall y\in Ay{<}_{s}t\leftrightarrow \neg \forall y\in Ay{<}_{s}x\right)$$
93	89 92	rexsn	$$⊢\exists t\in \left\{x\right\}\neg \forall y\in Ay{<}_{s}t\leftrightarrow \neg \forall y\in Ay{<}_{s}x$$
94	88 93	sylib	Could not format ( ( ( A < -. A. y e. A y -. A. y e. A y
95	76	ad2antrr	Could not format ( ( ( A < A C_ No ) : No typesetting found for |- ( ( ( A < A C_ No ) with typecode |-
96	95	sselda	Could not format ( ( ( ( A < y e. No ) : No typesetting found for |- ( ( ( ( A < y e. No ) with typecode |-
97		slenlt	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to \left(x{\le }_{s}y\leftrightarrow \neg y{<}_{s}x\right)$$
98	9 96 97	syl2an2r	Could not format ( ( ( ( A < ( x <_s y <-> -. y ( x <_s y <-> -. y
99	98	rexbidva	Could not format ( ( ( A < ( E. y e. A x <_s y <-> E. y e. A -. y ( E. y e. A x <_s y <-> E. y e. A -. y
100		rexnal	$$⊢\exists y\in A\neg y{<}_{s}x\leftrightarrow \neg \forall y\in Ay{<}_{s}x$$
101	99 100	bitrdi	Could not format ( ( ( A < ( E. y e. A x <_s y <-> -. A. y e. A y ( E. y e. A x <_s y <-> -. A. y e. A y
102	94 101	mpbird	Could not format ( ( ( A < E. y e. A x <_s y ) : No typesetting found for |- ( ( ( A < E. y e. A x <_s y ) with typecode |-
103	102	ralrimiva	Could not format ( ( A < A. x e. ( _Left ` X ) E. y e. A x <_s y ) : No typesetting found for |- ( ( A < A. x e. ( _Left ` X ) E. y e. A x <_s y ) with typecode |-
104	1	onssneli	$$⊢\mathrm{bday}\left(A{|}_{s}B\right)\subseteq \mathrm{bday}\left(z\right)\to \neg \mathrm{bday}\left(z\right)\in \mathrm{bday}\left(A{|}_{s}B\right)$$
105		rightssold	Could not format ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) : No typesetting found for |- ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) with typecode |-
106	105	a1i	Could not format ( ( A < ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) ) : No typesetting found for |- ( ( A < ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) ) with typecode |-
107	106	sselda	Could not format ( ( ( A < z e. ( _Old ` ( bday ` X ) ) ) : No typesetting found for |- ( ( ( A < z e. ( _Old ` ( bday ` X ) ) ) with typecode |-
108		rightssno	Could not format ( _Right ` X ) C_ No : No typesetting found for |- ( _Right ` X ) C_ No with typecode |-
109	108	a1i	Could not format ( ( A < ( _Right ` X ) C_ No ) : No typesetting found for |- ( ( A < ( _Right ` X ) C_ No ) with typecode |-
110	109	sselda	Could not format ( ( ( A < z e. No ) : No typesetting found for |- ( ( ( A < z e. No ) with typecode |-
111		oldbday	$$⊢\left(\mathrm{bday}\left(X\right)\in \mathrm{On}\wedge z\in \mathrm{No}\right)\to \left(z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\leftrightarrow \mathrm{bday}\left(z\right)\in \mathrm{bday}\left(X\right)\right)$$
112	6 110 111	sylancr	Could not format ( ( ( A < ( z e. ( _Old ` ( bday ` X ) ) <-> ( bday ` z ) e. ( bday ` X ) ) ) : No typesetting found for |- ( ( ( A < ( z e. ( _Old ` ( bday ` X ) ) <-> ( bday ` z ) e. ( bday ` X ) ) ) with typecode |-
113	107 112	mpbid	Could not format ( ( ( A < ( bday ` z ) e. ( bday ` X ) ) : No typesetting found for |- ( ( ( A < ( bday ` z ) e. ( bday ` X ) ) with typecode |-
114		simplr	Could not format ( ( ( A < X = ( A |s B ) ) : No typesetting found for |- ( ( ( A < X = ( A |s B ) ) with typecode |-
115	114	fveq2d	Could not format ( ( ( A < ( bday ` X ) = ( bday ` ( A |s B ) ) ) : No typesetting found for |- ( ( ( A < ( bday ` X ) = ( bday ` ( A |s B ) ) ) with typecode |-
116	113 115	eleqtrd	Could not format ( ( ( A < ( bday ` z ) e. ( bday ` ( A |s B ) ) ) : No typesetting found for |- ( ( ( A < ( bday ` z ) e. ( bday ` ( A |s B ) ) ) with typecode |-
117	104 116	nsyl3	Could not format ( ( ( A < -. ( bday ` ( A |s B ) ) C_ ( bday ` z ) ) : No typesetting found for |- ( ( ( A < -. ( bday ` ( A |s B ) ) C_ ( bday ` z ) ) with typecode |-
118	17	ad3antrrr	Could not format ( ( ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A <
119		sneq	$$⊢t=z\to \left\{t\right\}=\left\{z\right\}$$
120	119	breq2d	$$⊢t=z\to \left(A{\ll }_s\left\{t\right\}\leftrightarrow A{\ll }_s\left\{z\right\}\right)$$
121	119	breq1d	$$⊢t=z\to \left(\left\{t\right\}{\ll }_{s}B\leftrightarrow \left\{z\right\}{\ll }_{s}B\right)$$
122	120 121	anbi12d	$$⊢t=z\to \left(\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\leftrightarrow \left(A{\ll }_s\left\{z\right\}\wedge \left\{z\right\}{\ll }_{s}B\right)\right)$$
123	110	adantr	Could not format ( ( ( ( A < z e. No ) : No typesetting found for |- ( ( ( ( A < z e. No ) with typecode |-
124	73	ad2antrr	Could not format ( ( ( A < A e. _V ) : No typesetting found for |- ( ( ( A < A e. _V ) with typecode |-
125		vsnex	$$⊢\left\{z\right\}\in \mathrm{V}$$
126	125	a1i	Could not format ( ( ( A < { z } e. _V ) : No typesetting found for |- ( ( ( A < { z } e. _V ) with typecode |-
127	76	ad2antrr	Could not format ( ( ( A < A C_ No ) : No typesetting found for |- ( ( ( A < A C_ No ) with typecode |-
128	110	snssd	Could not format ( ( ( A < { z } C_ No ) : No typesetting found for |- ( ( ( A < { z } C_ No ) with typecode |-
129	127	sselda	Could not format ( ( ( ( A < a e. No ) : No typesetting found for |- ( ( ( ( A < a e. No ) with typecode |-
130	37	ad2antrr	Could not format ( ( ( ( A < X e. No ) : No typesetting found for |- ( ( ( ( A < X e. No ) with typecode |-
131	110	adantr	Could not format ( ( ( ( A < z e. No ) : No typesetting found for |- ( ( ( ( A < z e. No ) with typecode |-
132	48	ad2antrr	Could not format ( ( ( A < ( ( A |s B ) e. No /\ A < ( ( A |s B ) e. No /\ A <
133	132	simp2d	Could not format ( ( ( A < A < A <
134		ssltsepc	$$⊢\left(A{\ll }_s\left\{A{|}_{s}B\right\}\wedge a\in A\wedge A{|}_{s}B\in \left\{A{|}_{s}B\right\}\right)\to a{<}_s\left(A{|}_{s}B\right)$$
135	52 134	mp3an3	$$⊢\left(A{\ll }_s\left\{A{|}_{s}B\right\}\wedge a\in A\right)\to a{<}_s\left(A{|}_{s}B\right)$$
136	133 135	sylan	Could not format ( ( ( ( A < a a
137		simpllr	Could not format ( ( ( ( A < X = ( A |s B ) ) : No typesetting found for |- ( ( ( ( A < X = ( A |s B ) ) with typecode |-
138	136 137	breqtrrd	Could not format ( ( ( ( A < a a
139		rightval	Could not format ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
140	139	a1i	Could not format ( ( A < ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
141	140	eleq2d	Could not format ( ( A < ( z e. ( _Right ` X ) <-> z e. { z e. ( _Old ` ( bday ` X ) ) | X ( z e. ( _Right ` X ) <-> z e. { z e. ( _Old ` ( bday ` X ) ) | X
142		rabid	$$⊢z\in \left\{z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|X{<}_{s}z\right\}\leftrightarrow \left(z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge X{<}_{s}z\right)$$
143	141 142	bitrdi	Could not format ( ( A < ( z e. ( _Right ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X ( z e. ( _Right ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X
144	143	simplbda	Could not format ( ( ( A < X X
145	144	adantr	Could not format ( ( ( ( A < X X
146	129 130 131 138 145	slttrd	Could not format ( ( ( ( A < a a
147	146	3adant3	Could not format ( ( ( ( A < a a
148		velsn	$$⊢b\in \left\{z\right\}\leftrightarrow b=z$$
149		breq2	$$⊢b=z\to \left(a{<}_{s}b\leftrightarrow a{<}_{s}z\right)$$
150	148 149	sylbi	$$⊢b\in \left\{z\right\}\to \left(a{<}_{s}b\leftrightarrow a{<}_{s}z\right)$$
151	150	3ad2ant3	Could not format ( ( ( ( A < ( a a ( a a
152	147 151	mpbird	Could not format ( ( ( ( A < a a
153	124 126 127 128 152	ssltd	Could not format ( ( ( A < A < A <
154	153	anim1i	Could not format ( ( ( ( A < ( A < ( A <
155	122 123 154	elrabd	Could not format ( ( ( ( A < z e. { t e. No | ( A < z e. { t e. No | ( A <
156		fnfvima	$$⊢\left(\mathrm{bday}Fn\mathrm{No}\wedge \left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\subseteq \mathrm{No}\wedge z\in \left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right)\to \mathrm{bday}\left(z\right)\in \mathrm{bday}\left[\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right]$$
157	19 20 155 156	mp3an12i	Could not format ( ( ( ( A < ( bday ` z ) e. ( bday " { t e. No | ( A < ( bday ` z ) e. ( bday " { t e. No | ( A <
158		intss1	$$⊢\mathrm{bday}\left(z\right)\in \mathrm{bday}\left[\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right]\to \bigcap \mathrm{bday}\left[\left\{t\in \mathrm{No}|\left(A{\ll }_s\left\{t\right\}\wedge \left\{t\right\}{\ll }_{s}B\right)\right\}\right]\subseteq \mathrm{bday}\left(z\right)$$
159	157 158	syl	Could not format ( ( ( ( A < |^| ( bday " { t e. No | ( A < |^| ( bday " { t e. No | ( A <
160	118 159	eqsstrd	Could not format ( ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` z ) ) : No typesetting found for |- ( ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` z ) ) with typecode |-
161	117 160	mtand	Could not format ( ( ( A < -. { z } < -. { z } <
162	28	ad3antrrr	Could not format ( ( ( ( A < B e. _V ) : No typesetting found for |- ( ( ( ( A < B e. _V ) with typecode |-
163	162 125	jctil	Could not format ( ( ( ( A < ( { z } e. _V /\ B e. _V ) ) : No typesetting found for |- ( ( ( ( A < ( { z } e. _V /\ B e. _V ) ) with typecode |-
164	128	adantr	Could not format ( ( ( ( A < { z } C_ No ) : No typesetting found for |- ( ( ( ( A < { z } C_ No ) with typecode |-
165	31	ad3antrrr	Could not format ( ( ( ( A < B C_ No ) : No typesetting found for |- ( ( ( ( A < B C_ No ) with typecode |-
166		simpr	Could not format ( ( ( ( A < A. t e. { z } A. w e. B t A. t e. { z } A. w e. B t
167	164 165 166	3jca	Could not format ( ( ( ( A < ( { z } C_ No /\ B C_ No /\ A. t e. { z } A. w e. B t ( { z } C_ No /\ B C_ No /\ A. t e. { z } A. w e. B t
168		brsslt	$$⊢\left\{z\right\}{\ll }_{s}B\leftrightarrow \left(\left(\left\{z\right\}\in \mathrm{V}\wedge B\in \mathrm{V}\right)\wedge \left(\left\{z\right\}\subseteq \mathrm{No}\wedge B\subseteq \mathrm{No}\wedge \forall t\in \left\{z\right\}\forall w\in Bt{<}_{s}w\right)\right)$$
169	163 167 168	sylanbrc	Could not format ( ( ( ( A < { z } < { z } <
170	161 169	mtand	Could not format ( ( ( A < -. A. t e. { z } A. w e. B t -. A. t e. { z } A. w e. B t
171		rexnal	$$⊢\exists t\in \left\{z\right\}\neg \forall w\in Bt{<}_{s}w\leftrightarrow \neg \forall t\in \left\{z\right\}\forall w\in Bt{<}_{s}w$$
172	170 171	sylibr	Could not format ( ( ( A < E. t e. { z } -. A. w e. B t E. t e. { z } -. A. w e. B t
173		vex	$$⊢z\in \mathrm{V}$$
174		breq1	$$⊢t=z\to \left(t{<}_{s}w\leftrightarrow z{<}_{s}w\right)$$
175	174	ralbidv	$$⊢t=z\to \left(\forall w\in Bt{<}_{s}w\leftrightarrow \forall w\in Bz{<}_{s}w\right)$$
176	175	notbid	$$⊢t=z\to \left(\neg \forall w\in Bt{<}_{s}w\leftrightarrow \neg \forall w\in Bz{<}_{s}w\right)$$
177	173 176	rexsn	$$⊢\exists t\in \left\{z\right\}\neg \forall w\in Bt{<}_{s}w\leftrightarrow \neg \forall w\in Bz{<}_{s}w$$
178	172 177	sylib	Could not format ( ( ( A < -. A. w e. B z -. A. w e. B z
179	31	ad2antrr	Could not format ( ( ( A < B C_ No ) : No typesetting found for |- ( ( ( A < B C_ No ) with typecode |-
180	179	sselda	Could not format ( ( ( ( A < w e. No ) : No typesetting found for |- ( ( ( ( A < w e. No ) with typecode |-
181	110	adantr	Could not format ( ( ( ( A < z e. No ) : No typesetting found for |- ( ( ( ( A < z e. No ) with typecode |-
182		slenlt	$$⊢\left(w\in \mathrm{No}\wedge z\in \mathrm{No}\right)\to \left(w{\le }_{s}z\leftrightarrow \neg z{<}_{s}w\right)$$
183	180 181 182	syl2anc	Could not format ( ( ( ( A < ( w <_s z <-> -. z ( w <_s z <-> -. z
184	183	rexbidva	Could not format ( ( ( A < ( E. w e. B w <_s z <-> E. w e. B -. z ( E. w e. B w <_s z <-> E. w e. B -. z
185		rexnal	$$⊢\exists w\in B\neg z{<}_{s}w\leftrightarrow \neg \forall w\in Bz{<}_{s}w$$
186	184 185	bitrdi	Could not format ( ( ( A < ( E. w e. B w <_s z <-> -. A. w e. B z ( E. w e. B w <_s z <-> -. A. w e. B z
187	178 186	mpbird	Could not format ( ( ( A < E. w e. B w <_s z ) : No typesetting found for |- ( ( ( A < E. w e. B w <_s z ) with typecode |-
188	187	ralrimiva	Could not format ( ( A < A. z e. ( _Right ` X ) E. w e. B w <_s z ) : No typesetting found for |- ( ( A < A. z e. ( _Right ` X ) E. w e. B w <_s z ) with typecode |-
189	103 188	jca	Could not format ( ( A < ( A. x e. ( _Left ` X ) E. y e. A x <_s y /\ A. z e. ( _Right ` X ) E. w e. B w <_s z ) ) : No typesetting found for |- ( ( A < ( A. x e. ( _Left ` X ) E. y e. A x <_s y /\ A. z e. ( _Right ` X ) E. w e. B w <_s z ) ) with typecode |-