This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pclfinclN

Description: The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN and also pclcmpatN . (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfincl.a 
|- A = ( Atoms ` K )
pclfincl.c 
|- U = ( PCl ` K )
pclfincl.s 
|- S = ( PSubCl ` K )
Assertion pclfinclN 
|- ( ( K e. HL /\ X C_ A /\ X e. Fin ) -> ( U ` X ) e. S )

Proof

Step Hyp Ref Expression
1 pclfincl.a 
 |-  A = ( Atoms ` K )
2 pclfincl.c 
 |-  U = ( PCl ` K )
3 pclfincl.s 
 |-  S = ( PSubCl ` K )
4 sseq1 
 |-  ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
5 4 anbi2d 
 |-  ( x = (/) -> ( ( K e. HL /\ x C_ A ) <-> ( K e. HL /\ (/) C_ A ) ) )
6 fveq2 
 |-  ( x = (/) -> ( U ` x ) = ( U ` (/) ) )
7 6 eleq1d 
 |-  ( x = (/) -> ( ( U ` x ) e. S <-> ( U ` (/) ) e. S ) )
8 5 7 imbi12d 
 |-  ( x = (/) -> ( ( ( K e. HL /\ x C_ A ) -> ( U ` x ) e. S ) <-> ( ( K e. HL /\ (/) C_ A ) -> ( U ` (/) ) e. S ) ) )
9 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
10 9 anbi2d 
 |-  ( x = y -> ( ( K e. HL /\ x C_ A ) <-> ( K e. HL /\ y C_ A ) ) )
11 fveq2 
 |-  ( x = y -> ( U ` x ) = ( U ` y ) )
12 11 eleq1d 
 |-  ( x = y -> ( ( U ` x ) e. S <-> ( U ` y ) e. S ) )
13 10 12 imbi12d 
 |-  ( x = y -> ( ( ( K e. HL /\ x C_ A ) -> ( U ` x ) e. S ) <-> ( ( K e. HL /\ y C_ A ) -> ( U ` y ) e. S ) ) )
14 sseq1 
 |-  ( x = ( y u. { z } ) -> ( x C_ A <-> ( y u. { z } ) C_ A ) )
15 14 anbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( K e. HL /\ x C_ A ) <-> ( K e. HL /\ ( y u. { z } ) C_ A ) ) )
16 fveq2 
 |-  ( x = ( y u. { z } ) -> ( U ` x ) = ( U ` ( y u. { z } ) ) )
17 16 eleq1d 
 |-  ( x = ( y u. { z } ) -> ( ( U ` x ) e. S <-> ( U ` ( y u. { z } ) ) e. S ) )
18 15 17 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( K e. HL /\ x C_ A ) -> ( U ` x ) e. S ) <-> ( ( K e. HL /\ ( y u. { z } ) C_ A ) -> ( U ` ( y u. { z } ) ) e. S ) ) )
19 sseq1 
 |-  ( x = X -> ( x C_ A <-> X C_ A ) )
20 19 anbi2d 
 |-  ( x = X -> ( ( K e. HL /\ x C_ A ) <-> ( K e. HL /\ X C_ A ) ) )
21 fveq2 
 |-  ( x = X -> ( U ` x ) = ( U ` X ) )
22 21 eleq1d 
 |-  ( x = X -> ( ( U ` x ) e. S <-> ( U ` X ) e. S ) )
23 20 22 imbi12d 
 |-  ( x = X -> ( ( ( K e. HL /\ x C_ A ) -> ( U ` x ) e. S ) <-> ( ( K e. HL /\ X C_ A ) -> ( U ` X ) e. S ) ) )
24 2 pcl0N 
 |-  ( K e. HL -> ( U ` (/) ) = (/) )
25 3 0psubclN 
 |-  ( K e. HL -> (/) e. S )
26 24 25 eqeltrd 
 |-  ( K e. HL -> ( U ` (/) ) e. S )
27 26 adantr 
 |-  ( ( K e. HL /\ (/) C_ A ) -> ( U ` (/) ) e. S )
28 anass 
 |-  ( ( ( K e. HL /\ y C_ A ) /\ z e. A ) <-> ( K e. HL /\ ( y C_ A /\ z e. A ) ) )
29 vex 
 |-  z e. _V
30 29 snss 
 |-  ( z e. A <-> { z } C_ A )
31 30 anbi2i 
 |-  ( ( y C_ A /\ z e. A ) <-> ( y C_ A /\ { z } C_ A ) )
32 unss 
 |-  ( ( y C_ A /\ { z } C_ A ) <-> ( y u. { z } ) C_ A )
33 31 32 bitri 
 |-  ( ( y C_ A /\ z e. A ) <-> ( y u. { z } ) C_ A )
34 33 anbi2i 
 |-  ( ( K e. HL /\ ( y C_ A /\ z e. A ) ) <-> ( K e. HL /\ ( y u. { z } ) C_ A ) )
35 28 34 bitr2i 
 |-  ( ( K e. HL /\ ( y u. { z } ) C_ A ) <-> ( ( K e. HL /\ y C_ A ) /\ z e. A ) )
36 simpllr 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> y = (/) )
37 36 uneq1d 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( y u. { z } ) = ( (/) u. { z } ) )
38 uncom 
 |-  ( (/) u. { z } ) = ( { z } u. (/) )
39 un0 
 |-  ( { z } u. (/) ) = { z }
40 38 39 eqtri 
 |-  ( (/) u. { z } ) = { z }
41 37 40 eqtrdi 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( y u. { z } ) = { z } )
42 41 fveq2d 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( y u. { z } ) ) = ( U ` { z } ) )
43 simplrl 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> K e. HL )
44 hlatl 
 |-  ( K e. HL -> K e. AtLat )
45 43 44 syl 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> K e. AtLat )
46 simprr 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> z e. A )
47 eqid 
 |-  ( PSubSp ` K ) = ( PSubSp ` K )
48 1 47 snatpsubN 
 |-  ( ( K e. AtLat /\ z e. A ) -> { z } e. ( PSubSp ` K ) )
49 45 46 48 syl2anc 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> { z } e. ( PSubSp ` K ) )
50 47 2 pclidN 
 |-  ( ( K e. HL /\ { z } e. ( PSubSp ` K ) ) -> ( U ` { z } ) = { z } )
51 43 49 50 syl2anc 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` { z } ) = { z } )
52 42 51 eqtrd 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( y u. { z } ) ) = { z } )
53 1 3 atpsubclN 
 |-  ( ( K e. HL /\ z e. A ) -> { z } e. S )
54 43 46 53 syl2anc 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> { z } e. S )
55 52 54 eqeltrd 
 |-  ( ( ( ( y e. Fin /\ y = (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( y u. { z } ) ) e. S )
56 55 exp43 
 |-  ( ( y e. Fin /\ y = (/) ) -> ( ( K e. HL /\ y C_ A ) -> ( ( U ` y ) e. S -> ( z e. A -> ( U ` ( y u. { z } ) ) e. S ) ) ) )
57 simplrl 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> K e. HL )
58 1 2 pclssidN 
 |-  ( ( K e. HL /\ y C_ A ) -> y C_ ( U ` y ) )
59 58 ad2antlr 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> y C_ ( U ` y ) )
60 unss1 
 |-  ( y C_ ( U ` y ) -> ( y u. { z } ) C_ ( ( U ` y ) u. { z } ) )
61 59 60 syl 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( y u. { z } ) C_ ( ( U ` y ) u. { z } ) )
62 simprl 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` y ) e. S )
63 1 3 psubclssatN 
 |-  ( ( K e. HL /\ ( U ` y ) e. S ) -> ( U ` y ) C_ A )
64 57 62 63 syl2anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` y ) C_ A )
65 snssi 
 |-  ( z e. A -> { z } C_ A )
66 65 ad2antll 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> { z } C_ A )
67 eqid 
 |-  ( +P ` K ) = ( +P ` K )
68 1 67 paddunssN 
 |-  ( ( K e. HL /\ ( U ` y ) C_ A /\ { z } C_ A ) -> ( ( U ` y ) u. { z } ) C_ ( ( U ` y ) ( +P ` K ) { z } ) )
69 57 64 66 68 syl3anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( U ` y ) u. { z } ) C_ ( ( U ` y ) ( +P ` K ) { z } ) )
70 61 69 sstrd 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( y u. { z } ) C_ ( ( U ` y ) ( +P ` K ) { z } ) )
71 1 67 paddssat 
 |-  ( ( K e. HL /\ ( U ` y ) C_ A /\ { z } C_ A ) -> ( ( U ` y ) ( +P ` K ) { z } ) C_ A )
72 57 64 66 71 syl3anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( U ` y ) ( +P ` K ) { z } ) C_ A )
73 1 2 pclssN 
 |-  ( ( K e. HL /\ ( y u. { z } ) C_ ( ( U ` y ) ( +P ` K ) { z } ) /\ ( ( U ` y ) ( +P ` K ) { z } ) C_ A ) -> ( U ` ( y u. { z } ) ) C_ ( U ` ( ( U ` y ) ( +P ` K ) { z } ) ) )
74 57 70 72 73 syl3anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( y u. { z } ) ) C_ ( U ` ( ( U ` y ) ( +P ` K ) { z } ) ) )
75 simprr 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> z e. A )
76 1 67 3 paddatclN 
 |-  ( ( K e. HL /\ ( U ` y ) e. S /\ z e. A ) -> ( ( U ` y ) ( +P ` K ) { z } ) e. S )
77 57 62 75 76 syl3anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( U ` y ) ( +P ` K ) { z } ) e. S )
78 47 3 psubclsubN 
 |-  ( ( K e. HL /\ ( ( U ` y ) ( +P ` K ) { z } ) e. S ) -> ( ( U ` y ) ( +P ` K ) { z } ) e. ( PSubSp ` K ) )
79 57 77 78 syl2anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( U ` y ) ( +P ` K ) { z } ) e. ( PSubSp ` K ) )
80 47 2 pclidN 
 |-  ( ( K e. HL /\ ( ( U ` y ) ( +P ` K ) { z } ) e. ( PSubSp ` K ) ) -> ( U ` ( ( U ` y ) ( +P ` K ) { z } ) ) = ( ( U ` y ) ( +P ` K ) { z } ) )
81 57 79 80 syl2anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( ( U ` y ) ( +P ` K ) { z } ) ) = ( ( U ` y ) ( +P ` K ) { z } ) )
82 74 81 sseqtrd 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( y u. { z } ) ) C_ ( ( U ` y ) ( +P ` K ) { z } ) )
83 57 hllatd 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> K e. Lat )
84 simpllr 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> y =/= (/) )
85 1 2 pcl0bN 
 |-  ( ( K e. HL /\ y C_ A ) -> ( ( U ` y ) = (/) <-> y = (/) ) )
86 85 ad2antlr 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( U ` y ) = (/) <-> y = (/) ) )
87 86 necon3bid 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( U ` y ) =/= (/) <-> y =/= (/) ) )
88 84 87 mpbird 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` y ) =/= (/) )
89 eqid 
 |-  ( le ` K ) = ( le ` K )
90 eqid 
 |-  ( join ` K ) = ( join ` K )
91 89 90 1 67 elpaddat 
 |-  ( ( ( K e. Lat /\ ( U ` y ) C_ A /\ z e. A ) /\ ( U ` y ) =/= (/) ) -> ( q e. ( ( U ` y ) ( +P ` K ) { z } ) <-> ( q e. A /\ E. p e. ( U ` y ) q ( le ` K ) ( p ( join ` K ) z ) ) ) )
92 83 64 75 88 91 syl31anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( q e. ( ( U ` y ) ( +P ` K ) { z } ) <-> ( q e. A /\ E. p e. ( U ` y ) q ( le ` K ) ( p ( join ` K ) z ) ) ) )
93 simp1rl 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) -> K e. HL )
94 93 3ad2ant1 
 |-  ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) -> K e. HL )
95 94 adantr 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> K e. HL )
96 simprl 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> w e. ( PSubSp ` K ) )
97 simpl13 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> q e. A )
98 unss 
 |-  ( ( y C_ w /\ { z } C_ w ) <-> ( y u. { z } ) C_ w )
99 simpl 
 |-  ( ( y C_ w /\ { z } C_ w ) -> y C_ w )
100 98 99 sylbir 
 |-  ( ( y u. { z } ) C_ w -> y C_ w )
101 100 ad2antll 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> y C_ w )
102 simpl2 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> p e. ( U ` y ) )
103 47 2 elpcliN 
 |-  ( ( ( K e. HL /\ y C_ w /\ w e. ( PSubSp ` K ) ) /\ p e. ( U ` y ) ) -> p e. w )
104 95 101 96 102 103 syl31anc 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> p e. w )
105 29 snss 
 |-  ( z e. w <-> { z } C_ w )
106 105 biimpri 
 |-  ( { z } C_ w -> z e. w )
107 106 adantl 
 |-  ( ( y C_ w /\ { z } C_ w ) -> z e. w )
108 98 107 sylbir 
 |-  ( ( y u. { z } ) C_ w -> z e. w )
109 108 ad2antll 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> z e. w )
110 simpl3 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> q ( le ` K ) ( p ( join ` K ) z ) )
111 89 90 1 47 psubspi2N 
 |-  ( ( ( K e. HL /\ w e. ( PSubSp ` K ) /\ q e. A ) /\ ( p e. w /\ z e. w /\ q ( le ` K ) ( p ( join ` K ) z ) ) ) -> q e. w )
112 95 96 97 104 109 110 111 syl33anc 
 |-  ( ( ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) /\ p e. ( U ` y ) /\ q ( le ` K ) ( p ( join ` K ) z ) ) /\ ( w e. ( PSubSp ` K ) /\ ( y u. { z } ) C_ w ) ) -> q e. w )
113 112 exp520 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) -> ( p e. ( U ` y ) -> ( q ( le ` K ) ( p ( join ` K ) z ) -> ( w e. ( PSubSp ` K ) -> ( ( y u. { z } ) C_ w -> q e. w ) ) ) ) )
114 113 rexlimdv 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) /\ q e. A ) -> ( E. p e. ( U ` y ) q ( le ` K ) ( p ( join ` K ) z ) -> ( w e. ( PSubSp ` K ) -> ( ( y u. { z } ) C_ w -> q e. w ) ) ) )
115 114 3expia 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( q e. A -> ( E. p e. ( U ` y ) q ( le ` K ) ( p ( join ` K ) z ) -> ( w e. ( PSubSp ` K ) -> ( ( y u. { z } ) C_ w -> q e. w ) ) ) ) )
116 115 impd 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( q e. A /\ E. p e. ( U ` y ) q ( le ` K ) ( p ( join ` K ) z ) ) -> ( w e. ( PSubSp ` K ) -> ( ( y u. { z } ) C_ w -> q e. w ) ) ) )
117 92 116 sylbid 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( q e. ( ( U ` y ) ( +P ` K ) { z } ) -> ( w e. ( PSubSp ` K ) -> ( ( y u. { z } ) C_ w -> q e. w ) ) ) )
118 117 ralrimdv 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( q e. ( ( U ` y ) ( +P ` K ) { z } ) -> A. w e. ( PSubSp ` K ) ( ( y u. { z } ) C_ w -> q e. w ) ) )
119 simplrr 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> y C_ A )
120 119 75 jca 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( y C_ A /\ z e. A ) )
121 120 33 sylib 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( y u. { z } ) C_ A )
122 vex 
 |-  q e. _V
123 1 47 2 122 elpclN 
 |-  ( ( K e. HL /\ ( y u. { z } ) C_ A ) -> ( q e. ( U ` ( y u. { z } ) ) <-> A. w e. ( PSubSp ` K ) ( ( y u. { z } ) C_ w -> q e. w ) ) )
124 57 121 123 syl2anc 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( q e. ( U ` ( y u. { z } ) ) <-> A. w e. ( PSubSp ` K ) ( ( y u. { z } ) C_ w -> q e. w ) ) )
125 118 124 sylibrd 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( q e. ( ( U ` y ) ( +P ` K ) { z } ) -> q e. ( U ` ( y u. { z } ) ) ) )
126 125 ssrdv 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( ( U ` y ) ( +P ` K ) { z } ) C_ ( U ` ( y u. { z } ) ) )
127 82 126 eqssd 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( y u. { z } ) ) = ( ( U ` y ) ( +P ` K ) { z } ) )
128 127 77 eqeltrd 
 |-  ( ( ( ( y e. Fin /\ y =/= (/) ) /\ ( K e. HL /\ y C_ A ) ) /\ ( ( U ` y ) e. S /\ z e. A ) ) -> ( U ` ( y u. { z } ) ) e. S )
129 128 exp43 
 |-  ( ( y e. Fin /\ y =/= (/) ) -> ( ( K e. HL /\ y C_ A ) -> ( ( U ` y ) e. S -> ( z e. A -> ( U ` ( y u. { z } ) ) e. S ) ) ) )
130 56 129 pm2.61dane 
 |-  ( y e. Fin -> ( ( K e. HL /\ y C_ A ) -> ( ( U ` y ) e. S -> ( z e. A -> ( U ` ( y u. { z } ) ) e. S ) ) ) )
131 130 a2d 
 |-  ( y e. Fin -> ( ( ( K e. HL /\ y C_ A ) -> ( U ` y ) e. S ) -> ( ( K e. HL /\ y C_ A ) -> ( z e. A -> ( U ` ( y u. { z } ) ) e. S ) ) ) )
132 131 imp4b 
 |-  ( ( y e. Fin /\ ( ( K e. HL /\ y C_ A ) -> ( U ` y ) e. S ) ) -> ( ( ( K e. HL /\ y C_ A ) /\ z e. A ) -> ( U ` ( y u. { z } ) ) e. S ) )
133 35 132 biimtrid 
 |-  ( ( y e. Fin /\ ( ( K e. HL /\ y C_ A ) -> ( U ` y ) e. S ) ) -> ( ( K e. HL /\ ( y u. { z } ) C_ A ) -> ( U ` ( y u. { z } ) ) e. S ) )
134 133 ex 
 |-  ( y e. Fin -> ( ( ( K e. HL /\ y C_ A ) -> ( U ` y ) e. S ) -> ( ( K e. HL /\ ( y u. { z } ) C_ A ) -> ( U ` ( y u. { z } ) ) e. S ) ) )
135 8 13 18 23 27 134 findcard2 
 |-  ( X e. Fin -> ( ( K e. HL /\ X C_ A ) -> ( U ` X ) e. S ) )
136 135 3impib 
 |-  ( ( X e. Fin /\ K e. HL /\ X C_ A ) -> ( U ` X ) e. S )
137 136 3coml 
 |-  ( ( K e. HL /\ X C_ A /\ X e. Fin ) -> ( U ` X ) e. S )