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	$⊢ (A ≪_{s} B \land X = A \|_{s} B) \to (\forall x \in L (X) \exists y \in A x \leq_{s} y \land \forall z \in R (X) \exists w \in B w \leq_{s} z)$

Proof

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

Metamath Proof Explorer

Theorem cofcutr

Proof