Theorem archiabllem2a

Description: Lemma for archiabl , which requires the group to be both left- and right-ordered. (Contributed by Thierry Arnoux, 13-Apr-2018)

	Ref	Expression
Hypotheses	archiabllem.b	$$⊢B={\mathrm{Base}}_W$$
	archiabllem.0	$$⊢\underset{\dot{}}{0}=0_W$$
	archiabllem.e	$$⊢\underset{\dot{}}{\le }={\le }_W$$
	archiabllem.t	$$⊢\underset{\dot{}}{<}={<}_W$$
	archiabllem.m	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	archiabllem.g	$$⊢\phi \to W\in \mathrm{oGrp}$$
	archiabllem.a	$$⊢\phi \to W\in \mathrm{Archi}$$
	archiabllem2.1	$$⊢\underset{\dot{}}{+}={+}_W$$
	archiabllem2.2	$$⊢\phi \to {opp}_{𝑔}\left(W\right)\in \mathrm{oGrp}$$
	archiabllem2.3	$$⊢\left(\phi \wedge a\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}a\right)\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)$$
	archiabllem2a.4	$$⊢\phi \to X\in B$$
	archiabllem2a.5	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
Assertion	archiabllem2a	$$⊢\phi \to \exists c\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)$$

Proof

Step	Hyp	Ref	Expression
1		archiabllem.b	$$⊢B={\mathrm{Base}}_W$$
2		archiabllem.0	$$⊢\underset{\dot{}}{0}=0_W$$
3		archiabllem.e	$$⊢\underset{\dot{}}{\le }={\le }_W$$
4		archiabllem.t	$$⊢\underset{\dot{}}{<}={<}_W$$
5		archiabllem.m	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		archiabllem.g	$$⊢\phi \to W\in \mathrm{oGrp}$$
7		archiabllem.a	$$⊢\phi \to W\in \mathrm{Archi}$$
8		archiabllem2.1	$$⊢\underset{\dot{}}{+}={+}_W$$
9		archiabllem2.2	$$⊢\phi \to {opp}_{𝑔}\left(W\right)\in \mathrm{oGrp}$$
10		archiabllem2.3	$$⊢\left(\phi \wedge a\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}a\right)\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)$$
11		archiabllem2a.4	$$⊢\phi \to X\in B$$
12		archiabllem2a.5	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
13		simpllr	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\right)\to b\in B$$
14		simplrl	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}b$$
15		simpr	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\right)\to \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X$$
16		breq2	$$⊢c=b\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}b\right)$$
17		id	$$⊢c=b\to c=b$$
18	17 17	oveq12d	$$⊢c=b\to c\underset{\dot{}}{+}c=b\underset{\dot{}}{+}b$$
19	18	breq1d	$$⊢c=b\to \left(\left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\leftrightarrow \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\right)$$
20	16 19	anbi12d	$$⊢c=b\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\right)\right)$$
21	20	rspcev	$$⊢\left(b\in B\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\right)\right)\to \exists c\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)$$
22	13 14 15 21	syl12anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge \left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\right)\to \exists c\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)$$
23		simplll	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \phi$$
24		ogrpgrp	$$⊢W\in \mathrm{oGrp}\to W\in \mathrm{Grp}$$
25	23 6 24	3syl	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to W\in \mathrm{Grp}$$
26	23 11	syl	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to X\in B$$
27		simpllr	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to b\in B$$
28		eqid	$$⊢{-}_W={-}_W$$
29	1 28	grpsubcl	$$⊢\left(W\in \mathrm{Grp}\wedge X\in B\wedge b\in B\right)\to X{-}_{W}b\in B$$
30	25 26 27 29	syl3anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to X{-}_{W}b\in B$$
31	1 2 28	grpsubid	$$⊢\left(W\in \mathrm{Grp}\wedge b\in B\right)\to b{-}_{W}b=\underset{\dot{}}{0}$$
32	25 27 31	syl2anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to b{-}_{W}b=\underset{\dot{}}{0}$$
33	23 6	syl	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to W\in \mathrm{oGrp}$$
34		simplrr	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to b\underset{\dot{}}{<}X$$
35	1 4 28	ogrpsublt	$$⊢\left(W\in \mathrm{oGrp}\wedge \left(b\in B\wedge X\in B\wedge b\in B\right)\wedge b\underset{\dot{}}{<}X\right)\to \left(b{-}_{W}b\right)\underset{\dot{}}{<}\left(X{-}_{W}b\right)$$
36	33 27 26 27 34 35	syl131anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(b{-}_{W}b\right)\underset{\dot{}}{<}\left(X{-}_{W}b\right)$$
37	32 36	eqbrtrrd	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}\left(X{-}_{W}b\right)$$
38	23 9	syl	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to {opp}_{𝑔}\left(W\right)\in \mathrm{oGrp}$$
39	1 8	grpcl	$$⊢\left(W\in \mathrm{Grp}\wedge b\in B\wedge b\in B\right)\to b\underset{\dot{}}{+}b\in B$$
40	25 27 27 39	syl3anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to b\underset{\dot{}}{+}b\in B$$
41		simpr	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)$$
42	1 4 28	ogrpsublt	$$⊢\left(W\in \mathrm{oGrp}\wedge \left(X\in B\wedge b\underset{\dot{}}{+}b\in B\wedge b\in B\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(X{-}_{W}b\right)\underset{\dot{}}{<}\left(\left(b\underset{\dot{}}{+}b\right){-}_{W}b\right)$$
43	33 26 40 27 41 42	syl131anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(X{-}_{W}b\right)\underset{\dot{}}{<}\left(\left(b\underset{\dot{}}{+}b\right){-}_{W}b\right)$$
44	1 8 28	grpaddsubass	$$⊢\left(W\in \mathrm{Grp}\wedge \left(b\in B\wedge b\in B\wedge b\in B\right)\right)\to \left(b\underset{\dot{}}{+}b\right){-}_{W}b=b\underset{\dot{}}{+}\left(b{-}_{W}b\right)$$
45	25 27 27 27 44	syl13anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(b\underset{\dot{}}{+}b\right){-}_{W}b=b\underset{\dot{}}{+}\left(b{-}_{W}b\right)$$
46	32	oveq2d	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to b\underset{\dot{}}{+}\left(b{-}_{W}b\right)=b\underset{\dot{}}{+}\underset{\dot{}}{0}$$
47	1 8 2	grprid	$$⊢\left(W\in \mathrm{Grp}\wedge b\in B\right)\to b\underset{\dot{}}{+}\underset{\dot{}}{0}=b$$
48	25 27 47	syl2anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to b\underset{\dot{}}{+}\underset{\dot{}}{0}=b$$
49	45 46 48	3eqtrd	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(b\underset{\dot{}}{+}b\right){-}_{W}b=b$$
50	43 49	breqtrd	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(X{-}_{W}b\right)\underset{\dot{}}{<}b$$
51	1 4 8 25 38 30 27 30 50	ogrpaddltrd	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{<}\left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}b\right)$$
52	1 8 28	grpnpcan	$$⊢\left(W\in \mathrm{Grp}\wedge X\in B\wedge b\in B\right)\to \left(X{-}_{W}b\right)\underset{\dot{}}{+}b=X$$
53	25 26 27 52	syl3anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(X{-}_{W}b\right)\underset{\dot{}}{+}b=X$$
54	51 53	breqtrd	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{<}X$$
55		ovexd	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\in \mathrm{V}$$
56	3 4	pltle	$$⊢\left(W\in \mathrm{Grp}\wedge \left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\in \mathrm{V}\wedge X\in B\right)\to \left(\left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{<}X\to \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{\le }X\right)$$
57	25 55 26 56	syl3anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(\left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{<}X\to \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{\le }X\right)$$
58	54 57	mpd	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{\le }X$$
59		breq2	$$⊢c=X{-}_{W}b\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}\left(X{-}_{W}b\right)\right)$$
60		id	$$⊢c=X{-}_{W}b\to c=X{-}_{W}b$$
61	60 60	oveq12d	$$⊢c=X{-}_{W}b\to c\underset{\dot{}}{+}c=\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)$$
62	61	breq1d	$$⊢c=X{-}_{W}b\to \left(\left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\leftrightarrow \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{\le }X\right)$$
63	59 62	anbi12d	$$⊢c=X{-}_{W}b\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}\left(X{-}_{W}b\right)\wedge \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{\le }X\right)\right)$$
64	63	rspcev	$$⊢\left(X{-}_{W}b\in B\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}\left(X{-}_{W}b\right)\wedge \left(\left(X{-}_{W}b\right)\underset{\dot{}}{+}\left(X{-}_{W}b\right)\right)\underset{\dot{}}{\le }X\right)\right)\to \exists c\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)$$
65	30 37 58 64	syl12anc	$$⊢\left(\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\wedge X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)\to \exists c\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)$$
66	6	ad2antrr	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to W\in \mathrm{oGrp}$$
67		isogrp	$$⊢W\in \mathrm{oGrp}\leftrightarrow \left(W\in \mathrm{Grp}\wedge W\in \mathrm{oMnd}\right)$$
68	67	simprbi	$$⊢W\in \mathrm{oGrp}\to W\in \mathrm{oMnd}$$
69		omndtos	$$⊢W\in \mathrm{oMnd}\to W\in \mathrm{Toset}$$
70	66 68 69	3syl	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to W\in \mathrm{Toset}$$
71	66 24	syl	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to W\in \mathrm{Grp}$$
72		simplr	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to b\in B$$
73	71 72 72 39	syl3anc	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to b\underset{\dot{}}{+}b\in B$$
74	11	ad2antrr	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to X\in B$$
75	1 3 4	tlt2	$$⊢\left(W\in \mathrm{Toset}\wedge b\underset{\dot{}}{+}b\in B\wedge X\in B\right)\to \left(\left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\vee X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)$$
76	70 73 74 75	syl3anc	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to \left(\left(b\underset{\dot{}}{+}b\right)\underset{\dot{}}{\le }X\vee X\underset{\dot{}}{<}\left(b\underset{\dot{}}{+}b\right)\right)$$
77	22 65 76	mpjaodan	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\to \exists c\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)$$
78	10	3expia	$$⊢\left(\phi \wedge a\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}a\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)\right)$$
79	78	ralrimiva	$$⊢\phi \to \forall a\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}a\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)\right)$$
80		breq2	$$⊢a=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}a\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)$$
81		breq2	$$⊢a=X\to \left(b\underset{\dot{}}{<}a\leftrightarrow b\underset{\dot{}}{<}X\right)$$
82	81	anbi2d	$$⊢a=X\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)$$
83	82	rexbidv	$$⊢a=X\to \left(\exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)\leftrightarrow \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)$$
84	80 83	imbi12d	$$⊢a=X\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}a\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\right)$$
85	84	rspcv	$$⊢X\in B\to \left(\forall a\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}a\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)\right)\right)$$
86	11 79 12 85	syl3c	$$⊢\phi \to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}X\right)$$
87	77 86	r19.29a	$$⊢\phi \to \exists c\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}c\wedge \left(c\underset{\dot{}}{+}c\right)\underset{\dot{}}{\le }X\right)$$