Metamath Proof Explorer


Theorem stoweidlem18

Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem18.1 _tD
stoweidlem18.2 tφ
stoweidlem18.3 F=tT1
stoweidlem18.4 T=J
stoweidlem18.5 φatTaA
stoweidlem18.6 φBClsdJ
stoweidlem18.7 φE+
stoweidlem18.8 φD=
Assertion stoweidlem18 φxAtT0xtxt1tDxt<EtB1E<xt

Proof

Step Hyp Ref Expression
1 stoweidlem18.1 _tD
2 stoweidlem18.2 tφ
3 stoweidlem18.3 F=tT1
4 stoweidlem18.4 T=J
5 stoweidlem18.5 φatTaA
6 stoweidlem18.6 φBClsdJ
7 stoweidlem18.7 φE+
8 stoweidlem18.8 φD=
9 1re 1
10 5 stoweidlem4 φ1tT1A
11 9 10 mpan2 φtT1A
12 3 11 eqeltrid φFA
13 0le1 01
14 simpr φtTtT
15 3 fvmpt2 tT1Ft=1
16 14 9 15 sylancl φtTFt=1
17 13 16 breqtrrid φtT0Ft
18 1le1 11
19 16 18 eqbrtrdi φtTFt1
20 17 19 jca φtT0FtFt1
21 20 ex φtT0FtFt1
22 2 21 ralrimi φtT0FtFt1
23 nfcv _t
24 1 23 nfeq tD=
25 24 rzalf D=tDFt<E
26 8 25 syl φtDFt<E
27 1red φ1
28 27 7 ltsubrpd φ1E<1
29 28 adantr φtB1E<1
30 4 cldss BClsdJBT
31 6 30 syl φBT
32 31 sselda φtBtT
33 32 9 15 sylancl φtBFt=1
34 29 33 breqtrrd φtB1E<Ft
35 34 ex φtB1E<Ft
36 2 35 ralrimi φtB1E<Ft
37 nfcv _tx
38 nfmpt1 _ttT1
39 3 38 nfcxfr _tF
40 37 39 nfeq tx=F
41 fveq1 x=Fxt=Ft
42 41 breq2d x=F0xt0Ft
43 41 breq1d x=Fxt1Ft1
44 42 43 anbi12d x=F0xtxt10FtFt1
45 40 44 ralbid x=FtT0xtxt1tT0FtFt1
46 41 breq1d x=Fxt<EFt<E
47 40 46 ralbid x=FtDxt<EtDFt<E
48 41 breq2d x=F1E<xt1E<Ft
49 40 48 ralbid x=FtB1E<xttB1E<Ft
50 45 47 49 3anbi123d x=FtT0xtxt1tDxt<EtB1E<xttT0FtFt1tDFt<EtB1E<Ft
51 50 rspcev FAtT0FtFt1tDFt<EtB1E<FtxAtT0xtxt1tDxt<EtB1E<xt
52 12 22 26 36 51 syl13anc φxAtT0xtxt1tDxt<EtB1E<xt