Theorem toslublem

Description: Lemma for toslub and xrsclat . (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by NM, 15-Sep-2018)

	Ref	Expression
Hypotheses	toslub.b	$$⊢B={\mathrm{Base}}_K$$
	toslub.l	$$⊢\underset{\dot{}}{<}={<}_K$$
	toslub.1	$$⊢\phi \to K\in \mathrm{Toset}$$
	toslub.2	$$⊢\phi \to A\subseteq B$$
	toslub.e	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	toslublem	$$⊢\left(\phi \wedge a\in B\right)\to \left(\left(\forall b\in Ab\underset{\dot{}}{\le }a\wedge \forall c\in B\left(\forall b\in Ab\underset{\dot{}}{\le }c\to a\underset{\dot{}}{\le }c\right)\right)\leftrightarrow \left(\forall b\in A\neg a\underset{\dot{}}{<}b\wedge \forall b\in B\left(b\underset{\dot{}}{<}a\to \exists d\in Ab\underset{\dot{}}{<}d\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		toslub.b	$$⊢B={\mathrm{Base}}_K$$
2		toslub.l	$$⊢\underset{\dot{}}{<}={<}_K$$
3		toslub.1	$$⊢\phi \to K\in \mathrm{Toset}$$
4		toslub.2	$$⊢\phi \to A\subseteq B$$
5		toslub.e	$$⊢\underset{\dot{}}{\le }={\le }_K$$
6	3	ad2antrr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge b\in A\right)\to K\in \mathrm{Toset}$$
7		simplr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge b\in A\right)\to a\in B$$
8	4	adantr	$$⊢\left(\phi \wedge a\in B\right)\to A\subseteq B$$
9	8	sselda	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge b\in A\right)\to b\in B$$
10	1 5 2	tltnle	$$⊢\left(K\in \mathrm{Toset}\wedge a\in B\wedge b\in B\right)\to \left(a\underset{\dot{}}{<}b\leftrightarrow \neg b\underset{\dot{}}{\le }a\right)$$
11	6 7 9 10	syl3anc	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge b\in A\right)\to \left(a\underset{\dot{}}{<}b\leftrightarrow \neg b\underset{\dot{}}{\le }a\right)$$
12	11	con2bid	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge b\in A\right)\to \left(b\underset{\dot{}}{\le }a\leftrightarrow \neg a\underset{\dot{}}{<}b\right)$$
13	12	ralbidva	$$⊢\left(\phi \wedge a\in B\right)\to \left(\forall b\in Ab\underset{\dot{}}{\le }a\leftrightarrow \forall b\in A\neg a\underset{\dot{}}{<}b\right)$$
14	4	ad2antrr	$$⊢\left(\left(\phi \wedge c\in B\right)\wedge b\in A\right)\to A\subseteq B$$
15		simpr	$$⊢\left(\left(\phi \wedge c\in B\right)\wedge b\in A\right)\to b\in A$$
16	14 15	sseldd	$$⊢\left(\left(\phi \wedge c\in B\right)\wedge b\in A\right)\to b\in B$$
17	1 5 2	tltnle	$$⊢\left(K\in \mathrm{Toset}\wedge c\in B\wedge b\in B\right)\to \left(c\underset{\dot{}}{<}b\leftrightarrow \neg b\underset{\dot{}}{\le }c\right)$$
18	3 17	syl3an1	$$⊢\left(\phi \wedge c\in B\wedge b\in B\right)\to \left(c\underset{\dot{}}{<}b\leftrightarrow \neg b\underset{\dot{}}{\le }c\right)$$
19	18	3expa	$$⊢\left(\left(\phi \wedge c\in B\right)\wedge b\in B\right)\to \left(c\underset{\dot{}}{<}b\leftrightarrow \neg b\underset{\dot{}}{\le }c\right)$$
20	19	con2bid	$$⊢\left(\left(\phi \wedge c\in B\right)\wedge b\in B\right)\to \left(b\underset{\dot{}}{\le }c\leftrightarrow \neg c\underset{\dot{}}{<}b\right)$$
21	16 20	syldan	$$⊢\left(\left(\phi \wedge c\in B\right)\wedge b\in A\right)\to \left(b\underset{\dot{}}{\le }c\leftrightarrow \neg c\underset{\dot{}}{<}b\right)$$
22	21	ralbidva	$$⊢\left(\phi \wedge c\in B\right)\to \left(\forall b\in Ab\underset{\dot{}}{\le }c\leftrightarrow \forall b\in A\neg c\underset{\dot{}}{<}b\right)$$
23		breq2	$$⊢b=d\to \left(c\underset{\dot{}}{<}b\leftrightarrow c\underset{\dot{}}{<}d\right)$$
24	23	notbid	$$⊢b=d\to \left(\neg c\underset{\dot{}}{<}b\leftrightarrow \neg c\underset{\dot{}}{<}d\right)$$
25	24	cbvralvw	$$⊢\forall b\in A\neg c\underset{\dot{}}{<}b\leftrightarrow \forall d\in A\neg c\underset{\dot{}}{<}d$$
26		ralnex	$$⊢\forall d\in A\neg c\underset{\dot{}}{<}d\leftrightarrow \neg \exists d\in Ac\underset{\dot{}}{<}d$$
27	25 26	bitri	$$⊢\forall b\in A\neg c\underset{\dot{}}{<}b\leftrightarrow \neg \exists d\in Ac\underset{\dot{}}{<}d$$
28	22 27	bitrdi	$$⊢\left(\phi \wedge c\in B\right)\to \left(\forall b\in Ab\underset{\dot{}}{\le }c\leftrightarrow \neg \exists d\in Ac\underset{\dot{}}{<}d\right)$$
29	28	adantlr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to \left(\forall b\in Ab\underset{\dot{}}{\le }c\leftrightarrow \neg \exists d\in Ac\underset{\dot{}}{<}d\right)$$
30	3	ad2antrr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to K\in \mathrm{Toset}$$
31		simpr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to c\in B$$
32		simplr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to a\in B$$
33	1 5 2	tltnle	$$⊢\left(K\in \mathrm{Toset}\wedge c\in B\wedge a\in B\right)\to \left(c\underset{\dot{}}{<}a\leftrightarrow \neg a\underset{\dot{}}{\le }c\right)$$
34	30 31 32 33	syl3anc	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to \left(c\underset{\dot{}}{<}a\leftrightarrow \neg a\underset{\dot{}}{\le }c\right)$$
35	34	con2bid	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to \left(a\underset{\dot{}}{\le }c\leftrightarrow \neg c\underset{\dot{}}{<}a\right)$$
36	29 35	imbi12d	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to \left(\left(\forall b\in Ab\underset{\dot{}}{\le }c\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \left(\neg \exists d\in Ac\underset{\dot{}}{<}d\to \neg c\underset{\dot{}}{<}a\right)\right)$$
37		con34b	$$⊢\left(c\underset{\dot{}}{<}a\to \exists d\in Ac\underset{\dot{}}{<}d\right)\leftrightarrow \left(\neg \exists d\in Ac\underset{\dot{}}{<}d\to \neg c\underset{\dot{}}{<}a\right)$$
38	36 37	bitr4di	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge c\in B\right)\to \left(\left(\forall b\in Ab\underset{\dot{}}{\le }c\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \left(c\underset{\dot{}}{<}a\to \exists d\in Ac\underset{\dot{}}{<}d\right)\right)$$
39	38	ralbidva	$$⊢\left(\phi \wedge a\in B\right)\to \left(\forall c\in B\left(\forall b\in Ab\underset{\dot{}}{\le }c\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \forall c\in B\left(c\underset{\dot{}}{<}a\to \exists d\in Ac\underset{\dot{}}{<}d\right)\right)$$
40		breq1	$$⊢b=c\to \left(b\underset{\dot{}}{<}a\leftrightarrow c\underset{\dot{}}{<}a\right)$$
41		breq1	$$⊢b=c\to \left(b\underset{\dot{}}{<}d\leftrightarrow c\underset{\dot{}}{<}d\right)$$
42	41	rexbidv	$$⊢b=c\to \left(\exists d\in Ab\underset{\dot{}}{<}d\leftrightarrow \exists d\in Ac\underset{\dot{}}{<}d\right)$$
43	40 42	imbi12d	$$⊢b=c\to \left(\left(b\underset{\dot{}}{<}a\to \exists d\in Ab\underset{\dot{}}{<}d\right)\leftrightarrow \left(c\underset{\dot{}}{<}a\to \exists d\in Ac\underset{\dot{}}{<}d\right)\right)$$
44	43	cbvralvw	$$⊢\forall b\in B\left(b\underset{\dot{}}{<}a\to \exists d\in Ab\underset{\dot{}}{<}d\right)\leftrightarrow \forall c\in B\left(c\underset{\dot{}}{<}a\to \exists d\in Ac\underset{\dot{}}{<}d\right)$$
45	39 44	bitr4di	$$⊢\left(\phi \wedge a\in B\right)\to \left(\forall c\in B\left(\forall b\in Ab\underset{\dot{}}{\le }c\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \forall b\in B\left(b\underset{\dot{}}{<}a\to \exists d\in Ab\underset{\dot{}}{<}d\right)\right)$$
46	13 45	anbi12d	$$⊢\left(\phi \wedge a\in B\right)\to \left(\left(\forall b\in Ab\underset{\dot{}}{\le }a\wedge \forall c\in B\left(\forall b\in Ab\underset{\dot{}}{\le }c\to a\underset{\dot{}}{\le }c\right)\right)\leftrightarrow \left(\forall b\in A\neg a\underset{\dot{}}{<}b\wedge \forall b\in B\left(b\underset{\dot{}}{<}a\to \exists d\in Ab\underset{\dot{}}{<}d\right)\right)\right)$$