Theorem eqscut3

Description: A variant of the simplicity theorem - if B lies between the cut sets of A but none of its options do, then A = B . Theorem 11 of Conway p. 23. (Contributed by Scott Fenton, 28-Nov-2025)

	Ref	Expression
Hypotheses	eqscut3.1	$$⊢\phi \to L{\ll }_{s}R$$
	eqscut3.2	$$⊢\phi \to M{\ll }_{s}S$$
	eqscut3.3	$$⊢\phi \to A=L{|}_{s}R$$
	eqscut3.4	$$⊢\phi \to B=M{|}_{s}S$$
	eqscut3.5	$$⊢\phi \to L{\ll }_s\left\{B\right\}$$
	eqscut3.6	$$⊢\phi \to \left\{B\right\}{\ll }_{s}R$$
	eqscut3.7	No typesetting found for |- ( ph -> A. xO e. ( M u. S ) -. ( L <
Assertion	eqscut3	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqscut3.1	$$⊢\phi \to L{\ll }_{s}R$$
2		eqscut3.2	$$⊢\phi \to M{\ll }_{s}S$$
3		eqscut3.3	$$⊢\phi \to A=L{|}_{s}R$$
4		eqscut3.4	$$⊢\phi \to B=M{|}_{s}S$$
5		eqscut3.5	$$⊢\phi \to L{\ll }_s\left\{B\right\}$$
6		eqscut3.6	$$⊢\phi \to \left\{B\right\}{\ll }_{s}R$$
7		eqscut3.7	Could not format ( ph -> A. xO e. ( M u. S ) -. ( L < A. xO e. ( M u. S ) -. ( L <
8		sneq	Could not format ( xO = zR -> { xO } = { zR } ) : No typesetting found for |- ( xO = zR -> { xO } = { zR } ) with typecode |-
9	8	breq2d	Could not format ( xO = zR -> ( L < L < ( L < L <
10	8	breq1d	Could not format ( xO = zR -> ( { xO } < { zR } < ( { xO } < { zR } <
11	9 10	anbi12d	Could not format ( xO = zR -> ( ( L < ( L < ( ( L < ( L <
12	11	notbid	Could not format ( xO = zR -> ( -. ( L < -. ( L < ( -. ( L < -. ( L <
13	7	adantr	Could not format ( ( ph /\ zR e. S ) -> A. xO e. ( M u. S ) -. ( L < A. xO e. ( M u. S ) -. ( L <
14		elun2	Could not format ( zR e. S -> zR e. ( M u. S ) ) : No typesetting found for |- ( zR e. S -> zR e. ( M u. S ) ) with typecode |-
15	14	adantl	Could not format ( ( ph /\ zR e. S ) -> zR e. ( M u. S ) ) : No typesetting found for |- ( ( ph /\ zR e. S ) -> zR e. ( M u. S ) ) with typecode |-
16	12 13 15	rspcdva	Could not format ( ( ph /\ zR e. S ) -> -. ( L < -. ( L <
17	5	ad2antrr	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> L < L <
18	4	sneqd	$$⊢\phi \to \left\{B\right\}=\left\{M{|}_{s}S\right\}$$
19		scutcut	$$⊢M{\ll }_{s}S\to \left(M{|}_{s}S\in \mathrm{No}\wedge M{\ll }_s\left\{M{|}_{s}S\right\}\wedge \left\{M{|}_{s}S\right\}{\ll }_{s}S\right)$$
20	2 19	syl	$$⊢\phi \to \left(M{|}_{s}S\in \mathrm{No}\wedge M{\ll }_s\left\{M{|}_{s}S\right\}\wedge \left\{M{|}_{s}S\right\}{\ll }_{s}S\right)$$
21	20	simp3d	$$⊢\phi \to \left\{M{|}_{s}S\right\}{\ll }_{s}S$$
22	18 21	eqbrtrd	$$⊢\phi \to \left\{B\right\}{\ll }_{s}S$$
23	22	ad2antrr	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { B } < { B } <
24		simplr	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> zR e. S ) : No typesetting found for |- ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> zR e. S ) with typecode |-
25	24	snssd	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } C_ S ) : No typesetting found for |- ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } C_ S ) with typecode |-
26		sssslt2	Could not format ( ( { B } < { B } < { B } <
27	23 25 26	syl2anc	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { B } < { B } <
28	2	scutcld	$$⊢\phi \to M{|}_{s}S\in \mathrm{No}$$
29	4 28	eqeltrd	$$⊢\phi \to B\in \mathrm{No}$$
30		snnzg	$$⊢B\in \mathrm{No}\to \left\{B\right\}\ne \varnothing$$
31	29 30	syl	$$⊢\phi \to \left\{B\right\}\ne \varnothing$$
32	31	ad2antrr	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { B } =/= (/) ) : No typesetting found for |- ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { B } =/= (/) ) with typecode |-
33		sslttr	Could not format ( ( L < L < L <
34	17 27 32 33	syl3anc	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> L < L <
35		snex	Could not format { zR } e. _V : No typesetting found for |- { zR } e. _V with typecode |-
36	35	a1i	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } e. _V ) : No typesetting found for |- ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } e. _V ) with typecode |-
37		ssltex2	$$⊢L{\ll }_{s}R\to R\in \mathrm{V}$$
38	1 37	syl	$$⊢\phi \to R\in \mathrm{V}$$
39	38	ad2antrr	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> R e. _V ) : No typesetting found for |- ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> R e. _V ) with typecode |-
40		ssltss2	Could not format ( { B } < { zR } C_ No ) : No typesetting found for |- ( { B } < { zR } C_ No ) with typecode |-
41	27 40	syl	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } C_ No ) : No typesetting found for |- ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } C_ No ) with typecode |-
42		ssltss2	$$⊢L{\ll }_{s}R\to R\subseteq \mathrm{No}$$
43	1 42	syl	$$⊢\phi \to R\subseteq \mathrm{No}$$
44	43	ad2antrr	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> R C_ No ) : No typesetting found for |- ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> R C_ No ) with typecode |-
45		simpll	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ( ph /\ zR e. S ) ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ( ph /\ zR e. S ) ) with typecode |-
46		ssltss2	$$⊢M{\ll }_{s}S\to S\subseteq \mathrm{No}$$
47	2 46	syl	$$⊢\phi \to S\subseteq \mathrm{No}$$
48	47	sselda	Could not format ( ( ph /\ zR e. S ) -> zR e. No ) : No typesetting found for |- ( ( ph /\ zR e. S ) -> zR e. No ) with typecode |-
49	45 48	syl	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR e. No ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR e. No ) with typecode |-
50		simplll	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ph ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ph ) with typecode |-
51	1	scutcld	$$⊢\phi \to L{|}_{s}R\in \mathrm{No}$$
52	3 51	eqeltrd	$$⊢\phi \to A\in \mathrm{No}$$
53	50 52	syl	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A e. No ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A e. No ) with typecode |-
54	44	sselda	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> xR e. No ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> xR e. No ) with typecode |-
55		simplr	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR <_s A ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR <_s A ) with typecode |-
56		scutcut	$$⊢L{\ll }_{s}R\to \left(L{|}_{s}R\in \mathrm{No}\wedge L{\ll }_s\left\{L{|}_{s}R\right\}\wedge \left\{L{|}_{s}R\right\}{\ll }_{s}R\right)$$
57	1 56	syl	$$⊢\phi \to \left(L{|}_{s}R\in \mathrm{No}\wedge L{\ll }_s\left\{L{|}_{s}R\right\}\wedge \left\{L{|}_{s}R\right\}{\ll }_{s}R\right)$$
58	57	simp3d	$$⊢\phi \to \left\{L{|}_{s}R\right\}{\ll }_{s}R$$
59	58	adantr	Could not format ( ( ph /\ zR e. S ) -> { ( L |s R ) } < { ( L |s R ) } <
60	59	ad2antrr	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> { ( L |s R ) } < { ( L |s R ) } <
61		ovex	$$⊢L{|}_{s}R\in \mathrm{V}$$
62	61	elsn2	$$⊢A\in \left\{L{|}_{s}R\right\}\leftrightarrow A=L{|}_{s}R$$
63	3 62	sylibr	$$⊢\phi \to A\in \left\{L{|}_{s}R\right\}$$
64	63	adantr	Could not format ( ( ph /\ zR e. S ) -> A e. { ( L |s R ) } ) : No typesetting found for |- ( ( ph /\ zR e. S ) -> A e. { ( L |s R ) } ) with typecode |-
65	64	ad2antrr	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A e. { ( L |s R ) } ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A e. { ( L |s R ) } ) with typecode |-
66		simpr	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> xR e. R ) : No typesetting found for |- ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> xR e. R ) with typecode |-
67	60 65 66	ssltsepcd	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A A
68	49 53 54 55 67	slelttrd	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR zR
69		velsn	Could not format ( x e. { zR } <-> x = zR ) : No typesetting found for |- ( x e. { zR } <-> x = zR ) with typecode |-
70		breq1	Could not format ( x = zR -> ( x zR ( x zR
71	69 70	sylbi	Could not format ( x e. { zR } -> ( x zR ( x zR
72	68 71	syl5ibrcom	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ( x e. { zR } -> x ( x e. { zR } -> x
73	72	ex	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> ( xR e. R -> ( x e. { zR } -> x ( xR e. R -> ( x e. { zR } -> x
74	73	com23	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> ( x e. { zR } -> ( xR e. R -> x ( x e. { zR } -> ( xR e. R -> x
75	74	3imp	Could not format ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ x e. { zR } /\ xR e. R ) -> x x
76	36 39 41 44 75	ssltd	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } < { zR } <
77	34 76	jca	Could not format ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> ( L < ( L <
78	16 77	mtand	Could not format ( ( ph /\ zR e. S ) -> -. zR <_s A ) : No typesetting found for |- ( ( ph /\ zR e. S ) -> -. zR <_s A ) with typecode |-
79	52	adantr	Could not format ( ( ph /\ zR e. S ) -> A e. No ) : No typesetting found for |- ( ( ph /\ zR e. S ) -> A e. No ) with typecode |-
80		sltnle	Could not format ( ( A e. No /\ zR e. No ) -> ( A -. zR <_s A ) ) : No typesetting found for |- ( ( A e. No /\ zR e. No ) -> ( A -. zR <_s A ) ) with typecode |-
81	79 48 80	syl2anc	Could not format ( ( ph /\ zR e. S ) -> ( A -. zR <_s A ) ) : No typesetting found for |- ( ( ph /\ zR e. S ) -> ( A -. zR <_s A ) ) with typecode |-
82	78 81	mpbird	Could not format ( ( ph /\ zR e. S ) -> A A
83	82	ralrimiva	Could not format ( ph -> A. zR e. S A A. zR e. S A
84		ssltsep	$$⊢L{\ll }_s\left\{B\right\}\to \forall x\in L\forall y\in \left\{B\right\}x{<}_{s}y$$
85	5 84	syl	$$⊢\phi \to \forall x\in L\forall y\in \left\{B\right\}x{<}_{s}y$$
86		breq2	$$⊢y=B\to \left(x{<}_{s}y\leftrightarrow x{<}_{s}B\right)$$
87	86	ralsng	$$⊢B\in \mathrm{No}\to \left(\forall y\in \left\{B\right\}x{<}_{s}y\leftrightarrow x{<}_{s}B\right)$$
88	29 87	syl	$$⊢\phi \to \left(\forall y\in \left\{B\right\}x{<}_{s}y\leftrightarrow x{<}_{s}B\right)$$
89	88	ralbidv	$$⊢\phi \to \left(\forall x\in L\forall y\in \left\{B\right\}x{<}_{s}y\leftrightarrow \forall x\in Lx{<}_{s}B\right)$$
90	85 89	mpbid	$$⊢\phi \to \forall x\in Lx{<}_{s}B$$
91	1 2 3 4	slerecd	Could not format ( ph -> ( A <_s B <-> ( A. zR e. S A ( A <_s B <-> ( A. zR e. S A
92	83 90 91	mpbir2and	$$⊢\phi \to A{\le }_{s}B$$
93		ssltsep	$$⊢\left\{B\right\}{\ll }_{s}R\to \forall x\in \left\{B\right\}\forall y\in Rx{<}_{s}y$$
94	6 93	syl	$$⊢\phi \to \forall x\in \left\{B\right\}\forall y\in Rx{<}_{s}y$$
95		breq1	$$⊢x=B\to \left(x{<}_{s}y\leftrightarrow B{<}_{s}y\right)$$
96	95	ralbidv	$$⊢x=B\to \left(\forall y\in Rx{<}_{s}y\leftrightarrow \forall y\in RB{<}_{s}y\right)$$
97	96	ralsng	$$⊢B\in \mathrm{No}\to \left(\forall x\in \left\{B\right\}\forall y\in Rx{<}_{s}y\leftrightarrow \forall y\in RB{<}_{s}y\right)$$
98	29 97	syl	$$⊢\phi \to \left(\forall x\in \left\{B\right\}\forall y\in Rx{<}_{s}y\leftrightarrow \forall y\in RB{<}_{s}y\right)$$
99	94 98	mpbid	$$⊢\phi \to \forall y\in RB{<}_{s}y$$
100		sneq	Could not format ( xO = zL -> { xO } = { zL } ) : No typesetting found for |- ( xO = zL -> { xO } = { zL } ) with typecode |-
101	100	breq2d	Could not format ( xO = zL -> ( L < L < ( L < L <
102	100	breq1d	Could not format ( xO = zL -> ( { xO } < { zL } < ( { xO } < { zL } <
103	101 102	anbi12d	Could not format ( xO = zL -> ( ( L < ( L < ( ( L < ( L <
104	103	notbid	Could not format ( xO = zL -> ( -. ( L < -. ( L < ( -. ( L < -. ( L <
105	7	adantr	Could not format ( ( ph /\ zL e. M ) -> A. xO e. ( M u. S ) -. ( L < A. xO e. ( M u. S ) -. ( L <
106		elun1	Could not format ( zL e. M -> zL e. ( M u. S ) ) : No typesetting found for |- ( zL e. M -> zL e. ( M u. S ) ) with typecode |-
107	106	adantl	Could not format ( ( ph /\ zL e. M ) -> zL e. ( M u. S ) ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> zL e. ( M u. S ) ) with typecode |-
108	104 105 107	rspcdva	Could not format ( ( ph /\ zL e. M ) -> -. ( L < -. ( L <
109		ssltex1	$$⊢L{\ll }_{s}R\to L\in \mathrm{V}$$
110	1 109	syl	$$⊢\phi \to L\in \mathrm{V}$$
111	110	ad2antrr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L e. _V ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L e. _V ) with typecode |-
112		snex	Could not format { zL } e. _V : No typesetting found for |- { zL } e. _V with typecode |-
113	112	a1i	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } e. _V ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } e. _V ) with typecode |-
114		ssltss1	$$⊢L{\ll }_{s}R\to L\subseteq \mathrm{No}$$
115	1 114	syl	$$⊢\phi \to L\subseteq \mathrm{No}$$
116	115	adantr	Could not format ( ( ph /\ zL e. M ) -> L C_ No ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> L C_ No ) with typecode |-
117	116	adantr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L C_ No ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L C_ No ) with typecode |-
118		simplr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> zL e. M ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> zL e. M ) with typecode |-
119	118	snssd	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } C_ M ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } C_ M ) with typecode |-
120		ssltss1	$$⊢M{\ll }_{s}S\to M\subseteq \mathrm{No}$$
121	2 120	syl	$$⊢\phi \to M\subseteq \mathrm{No}$$
122	121	ad2antrr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> M C_ No ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> M C_ No ) with typecode |-
123	119 122	sstrd	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } C_ No ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } C_ No ) with typecode |-
124	117	sselda	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL e. No ) : No typesetting found for |- ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL e. No ) with typecode |-
125		simplll	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> ph ) : No typesetting found for |- ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> ph ) with typecode |-
126	125 52	syl	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A e. No ) : No typesetting found for |- ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A e. No ) with typecode |-
127	121	sselda	Could not format ( ( ph /\ zL e. M ) -> zL e. No ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> zL e. No ) with typecode |-
128	127	adantr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> zL e. No ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> zL e. No ) with typecode |-
129	128	adantr	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> zL e. No ) : No typesetting found for |- ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> zL e. No ) with typecode |-
130	57	simp2d	$$⊢\phi \to L{\ll }_s\left\{L{|}_{s}R\right\}$$
131	130	adantr	Could not format ( ( ph /\ zL e. M ) -> L < L <
132	131	adantr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L < L <
133	132	adantr	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> L < L <
134		simpr	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL e. L ) : No typesetting found for |- ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL e. L ) with typecode |-
135	63	adantr	Could not format ( ( ph /\ zL e. M ) -> A e. { ( L |s R ) } ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> A e. { ( L |s R ) } ) with typecode |-
136	135	adantr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> A e. { ( L |s R ) } ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> A e. { ( L |s R ) } ) with typecode |-
137	136	adantr	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A e. { ( L |s R ) } ) : No typesetting found for |- ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A e. { ( L |s R ) } ) with typecode |-
138	133 134 137	ssltsepcd	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL xL
139		simplr	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A <_s zL ) : No typesetting found for |- ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A <_s zL ) with typecode |-
140	124 126 129 138 139	sltletrd	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL xL
141		velsn	Could not format ( x e. { zL } <-> x = zL ) : No typesetting found for |- ( x e. { zL } <-> x = zL ) with typecode |-
142		breq2	Could not format ( x = zL -> ( xL xL ( xL xL
143	141 142	sylbi	Could not format ( x e. { zL } -> ( xL xL ( xL xL
144	140 143	syl5ibrcom	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> ( x e. { zL } -> xL ( x e. { zL } -> xL
145	144	3impia	Could not format ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L /\ x e. { zL } ) -> xL xL
146	111 113 117 123 145	ssltd	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L < L <
147	20	simp2d	$$⊢\phi \to M{\ll }_s\left\{M{|}_{s}S\right\}$$
148	147 18	breqtrrd	$$⊢\phi \to M{\ll }_s\left\{B\right\}$$
149	148	adantr	Could not format ( ( ph /\ zL e. M ) -> M < M <
150	149	adantr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> M < M <
151		sssslt1	Could not format ( ( M < { zL } < { zL } <
152	150 119 151	syl2anc	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } < { zL } <
153		simpll	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> ph ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> ph ) with typecode |-
154	153 6	syl	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { B } < { B } <
155	31	adantr	Could not format ( ( ph /\ zL e. M ) -> { B } =/= (/) ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> { B } =/= (/) ) with typecode |-
156	155	adantr	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { B } =/= (/) ) : No typesetting found for |- ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { B } =/= (/) ) with typecode |-
157		sslttr	Could not format ( ( { zL } < { zL } < { zL } <
158	152 154 156 157	syl3anc	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } < { zL } <
159	146 158	jca	Could not format ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> ( L < ( L <
160	108 159	mtand	Could not format ( ( ph /\ zL e. M ) -> -. A <_s zL ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> -. A <_s zL ) with typecode |-
161	52	adantr	Could not format ( ( ph /\ zL e. M ) -> A e. No ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> A e. No ) with typecode |-
162		sltnle	Could not format ( ( zL e. No /\ A e. No ) -> ( zL -. A <_s zL ) ) : No typesetting found for |- ( ( zL e. No /\ A e. No ) -> ( zL -. A <_s zL ) ) with typecode |-
163	127 161 162	syl2anc	Could not format ( ( ph /\ zL e. M ) -> ( zL -. A <_s zL ) ) : No typesetting found for |- ( ( ph /\ zL e. M ) -> ( zL -. A <_s zL ) ) with typecode |-
164	160 163	mpbird	Could not format ( ( ph /\ zL e. M ) -> zL zL
165	164	ralrimiva	Could not format ( ph -> A. zL e. M zL A. zL e. M zL
166	2 1 4 3	slerecd	Could not format ( ph -> ( B <_s A <-> ( A. y e. R B ( B <_s A <-> ( A. y e. R B
167	99 165 166	mpbir2and	$$⊢\phi \to B{\le }_{s}A$$
168		sletri3	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A=B\leftrightarrow \left(A{\le }_{s}B\wedge B{\le }_{s}A\right)\right)$$
169	52 29 168	syl2anc	$$⊢\phi \to \left(A=B\leftrightarrow \left(A{\le }_{s}B\wedge B{\le }_{s}A\right)\right)$$
170	92 167 169	mpbir2and	$$⊢\phi \to A=B$$