Metamath Proof Explorer


Theorem lbsextlem3

Description: Lemma for lbsext . A chain in S has an upper bound in S . (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsext.v V = Base W
lbsext.j J = LBasis W
lbsext.n N = LSpan W
lbsext.w φ W LVec
lbsext.c φ C V
lbsext.x φ x C ¬ x N C x
lbsext.s S = z 𝒫 V | C z x z ¬ x N z x
lbsext.p P = LSubSp W
lbsext.a φ A S
lbsext.z φ A
lbsext.r φ [⊂] Or A
lbsext.t T = u A N u x
Assertion lbsextlem3 φ A S

Proof

Step Hyp Ref Expression
1 lbsext.v V = Base W
2 lbsext.j J = LBasis W
3 lbsext.n N = LSpan W
4 lbsext.w φ W LVec
5 lbsext.c φ C V
6 lbsext.x φ x C ¬ x N C x
7 lbsext.s S = z 𝒫 V | C z x z ¬ x N z x
8 lbsext.p P = LSubSp W
9 lbsext.a φ A S
10 lbsext.z φ A
11 lbsext.r φ [⊂] Or A
12 lbsext.t T = u A N u x
13 7 ssrab3 S 𝒫 V
14 9 13 sstrdi φ A 𝒫 V
15 sspwuni A 𝒫 V A V
16 14 15 sylib φ A V
17 1 fvexi V V
18 17 elpw2 A 𝒫 V A V
19 16 18 sylibr φ A 𝒫 V
20 ssintub C z 𝒫 V | C z
21 simpl C z x z ¬ x N z x C z
22 21 a1i z 𝒫 V C z x z ¬ x N z x C z
23 22 ss2rabi z 𝒫 V | C z x z ¬ x N z x z 𝒫 V | C z
24 7 23 eqsstri S z 𝒫 V | C z
25 9 24 sstrdi φ A z 𝒫 V | C z
26 intss A z 𝒫 V | C z z 𝒫 V | C z A
27 25 26 syl φ z 𝒫 V | C z A
28 20 27 sstrid φ C A
29 intssuni A A A
30 10 29 syl φ A A
31 28 30 sstrd φ C A
32 eluni2 x A y A x y
33 simpll1 φ y A x y u A x N u x φ
34 lveclmod W LVec W LMod
35 4 34 syl φ W LMod
36 33 35 syl φ y A x y u A x N u x W LMod
37 33 9 syl φ y A x y u A x N u x A S
38 33 11 syl φ y A x y u A x N u x [⊂] Or A
39 simpll2 φ y A x y u A x N u x y A
40 simplr φ y A x y u A x N u x u A
41 sorpssun [⊂] Or A y A u A y u A
42 38 39 40 41 syl12anc φ y A x y u A x N u x y u A
43 37 42 sseldd φ y A x y u A x N u x y u S
44 13 43 sseldi φ y A x y u A x N u x y u 𝒫 V
45 44 elpwid φ y A x y u A x N u x y u V
46 45 ssdifssd φ y A x y u A x N u x y u x V
47 ssun2 u y u
48 ssdif u y u u x y u x
49 47 48 mp1i φ y A x y u A x N u x u x y u x
50 1 3 lspss W LMod y u x V u x y u x N u x N y u x
51 36 46 49 50 syl3anc φ y A x y u A x N u x N u x N y u x
52 simpr φ y A x y u A x N u x x N u x
53 51 52 sseldd φ y A x y u A x N u x x N y u x
54 sseq2 z = y u C z C y u
55 difeq1 z = y u z x = y u x
56 55 fveq2d z = y u N z x = N y u x
57 56 eleq2d z = y u x N z x x N y u x
58 57 notbid z = y u ¬ x N z x ¬ x N y u x
59 58 raleqbi1dv z = y u x z ¬ x N z x x y u ¬ x N y u x
60 54 59 anbi12d z = y u C z x z ¬ x N z x C y u x y u ¬ x N y u x
61 60 7 elrab2 y u S y u 𝒫 V C y u x y u ¬ x N y u x
62 61 simprbi y u S C y u x y u ¬ x N y u x
63 62 simprd y u S x y u ¬ x N y u x
64 43 63 syl φ y A x y u A x N u x x y u ¬ x N y u x
65 simpll3 φ y A x y u A x N u x x y
66 elun1 x y x y u
67 65 66 syl φ y A x y u A x N u x x y u
68 rsp x y u ¬ x N y u x x y u ¬ x N y u x
69 64 67 68 sylc φ y A x y u A x N u x ¬ x N y u x
70 53 69 pm2.65da φ y A x y u A ¬ x N u x
71 70 nrexdv φ y A x y ¬ u A x N u x
72 1 2 3 4 5 6 7 8 9 10 11 12 lbsextlem2 φ T P A x T
73 72 simpld φ T P
74 1 8 lssss T P T V
75 73 74 syl φ T V
76 72 simprd φ A x T
77 1 3 lspss W LMod T V A x T N A x N T
78 35 75 76 77 syl3anc φ N A x N T
79 8 3 lspid W LMod T P N T = T
80 35 73 79 syl2anc φ N T = T
81 78 80 sseqtrd φ N A x T
82 81 3ad2ant1 φ y A x y N A x T
83 82 12 sseqtrdi φ y A x y N A x u A N u x
84 83 sseld φ y A x y x N A x x u A N u x
85 eliun x u A N u x u A x N u x
86 84 85 syl6ib φ y A x y x N A x u A x N u x
87 71 86 mtod φ y A x y ¬ x N A x
88 87 rexlimdv3a φ y A x y ¬ x N A x
89 32 88 syl5bi φ x A ¬ x N A x
90 89 ralrimiv φ x A ¬ x N A x
91 31 90 jca φ C A x A ¬ x N A x
92 sseq2 z = A C z C A
93 difeq1 z = A z x = A x
94 93 fveq2d z = A N z x = N A x
95 94 eleq2d z = A x N z x x N A x
96 95 notbid z = A ¬ x N z x ¬ x N A x
97 96 raleqbi1dv z = A x z ¬ x N z x x A ¬ x N A x
98 92 97 anbi12d z = A C z x z ¬ x N z x C A x A ¬ x N A x
99 98 7 elrab2 A S A 𝒫 V C A x A ¬ x N A x
100 19 91 99 sylanbrc φ A S