Metamath Proof Explorer

Theorem pclfinN

Description: The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of PtakPulmannova p. 72. Compare the closed subspace version pclfinclN . (Contributed by NM, 10-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfin.a 
|- A = ( Atoms ` K )
pclfin.c 
|- U = ( PCl ` K )
Assertion pclfinN 
|- ( ( K e. AtLat /\ X C_ A ) -> ( U ` X ) = U_ y e. ( Fin i^i ~P X ) ( U ` y ) )

Proof

Step Hyp Ref Expression
1 pclfin.a 
 |-  A = ( Atoms ` K )
2 pclfin.c 
 |-  U = ( PCl ` K )
3 simpl 
 |-  ( ( K e. AtLat /\ X C_ A ) -> K e. AtLat )
4 elin 
 |-  ( y e. ( Fin i^i ~P X ) <-> ( y e. Fin /\ y e. ~P X ) )
5 elpwi 
 |-  ( y e. ~P X -> y C_ X )
6 5 adantl 
 |-  ( ( y e. Fin /\ y e. ~P X ) -> y C_ X )
7 4 6 sylbi 
 |-  ( y e. ( Fin i^i ~P X ) -> y C_ X )
8 simpll 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> K e. AtLat )
9 sstr 
 |-  ( ( y C_ X /\ X C_ A ) -> y C_ A )
10 9 ancoms 
 |-  ( ( X C_ A /\ y C_ X ) -> y C_ A )
11 10 adantll 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> y C_ A )
12 eqid 
 |-  ( PSubSp ` K ) = ( PSubSp ` K )
13 1 12 2 pclclN 
 |-  ( ( K e. AtLat /\ y C_ A ) -> ( U ` y ) e. ( PSubSp ` K ) )
14 8 11 13 syl2anc 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( U ` y ) e. ( PSubSp ` K ) )
15 1 12 psubssat 
 |-  ( ( K e. AtLat /\ ( U ` y ) e. ( PSubSp ` K ) ) -> ( U ` y ) C_ A )
16 8 14 15 syl2anc 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( U ` y ) C_ A )
17 16 ex 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( y C_ X -> ( U ` y ) C_ A ) )
18 7 17 syl5 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( y e. ( Fin i^i ~P X ) -> ( U ` y ) C_ A ) )
19 18 ralrimiv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> A. y e. ( Fin i^i ~P X ) ( U ` y ) C_ A )
20 iunss 
 |-  ( U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ A <-> A. y e. ( Fin i^i ~P X ) ( U ` y ) C_ A )
21 19 20 sylibr 
 |-  ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ A )
22 eliun 
 |-  ( p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) p e. ( U ` y ) )
23 fveq2 
 |-  ( y = w -> ( U ` y ) = ( U ` w ) )
24 23 eleq2d 
 |-  ( y = w -> ( p e. ( U ` y ) <-> p e. ( U ` w ) ) )
25 24 cbvrexvw 
 |-  ( E. y e. ( Fin i^i ~P X ) p e. ( U ` y ) <-> E. w e. ( Fin i^i ~P X ) p e. ( U ` w ) )
26 22 25 bitri 
 |-  ( p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. w e. ( Fin i^i ~P X ) p e. ( U ` w ) )
27 eliun 
 |-  ( q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) q e. ( U ` y ) )
28 fveq2 
 |-  ( y = v -> ( U ` y ) = ( U ` v ) )
29 28 eleq2d 
 |-  ( y = v -> ( q e. ( U ` y ) <-> q e. ( U ` v ) ) )
30 29 cbvrexvw 
 |-  ( E. y e. ( Fin i^i ~P X ) q e. ( U ` y ) <-> E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) )
31 27 30 bitri 
 |-  ( q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) )
32 26 31 anbi12i 
 |-  ( ( p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) /\ q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) <-> ( E. w e. ( Fin i^i ~P X ) p e. ( U ` w ) /\ E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) ) )
33 elin 
 |-  ( w e. ( Fin i^i ~P X ) <-> ( w e. Fin /\ w e. ~P X ) )
34 elpwi 
 |-  ( w e. ~P X -> w C_ X )
35 34 anim2i 
 |-  ( ( w e. Fin /\ w e. ~P X ) -> ( w e. Fin /\ w C_ X ) )
36 33 35 sylbi 
 |-  ( w e. ( Fin i^i ~P X ) -> ( w e. Fin /\ w C_ X ) )
37 elin 
 |-  ( v e. ( Fin i^i ~P X ) <-> ( v e. Fin /\ v e. ~P X ) )
38 elpwi 
 |-  ( v e. ~P X -> v C_ X )
39 38 anim2i 
 |-  ( ( v e. Fin /\ v e. ~P X ) -> ( v e. Fin /\ v C_ X ) )
40 37 39 sylbi 
 |-  ( v e. ( Fin i^i ~P X ) -> ( v e. Fin /\ v C_ X ) )
41 simp2rl 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> w e. Fin )
42 simp12l 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> v e. Fin )
43 unfi 
 |-  ( ( w e. Fin /\ v e. Fin ) -> ( w u. v ) e. Fin )
44 41 42 43 syl2anc 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( w u. v ) e. Fin )
45 simp2rr 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> w C_ X )
46 simp12r 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> v C_ X )
47 45 46 unssd 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( w u. v ) C_ X )
48 vex 
 |-  w e. _V
49 vex 
 |-  v e. _V
50 48 49 unex 
 |-  ( w u. v ) e. _V
51 50 elpw 
 |-  ( ( w u. v ) e. ~P X <-> ( w u. v ) C_ X )
52 47 51 sylibr 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( w u. v ) e. ~P X )
53 44 52 elind 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( w u. v ) e. ( Fin i^i ~P X ) )
54 simp11l 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> K e. AtLat )
55 simp11r 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> X C_ A )
56 45 55 sstrd 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> w C_ A )
57 46 55 sstrd 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> v C_ A )
58 56 57 unssd 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( w u. v ) C_ A )
59 1 12 2 pclclN 
 |-  ( ( K e. AtLat /\ ( w u. v ) C_ A ) -> ( U ` ( w u. v ) ) e. ( PSubSp ` K ) )
60 54 58 59 syl2anc 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( U ` ( w u. v ) ) e. ( PSubSp ` K ) )
61 simp3l 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> r e. A )
62 ssun1 
 |-  w C_ ( w u. v )
63 62 a1i 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> w C_ ( w u. v ) )
64 1 2 pclssN 
 |-  ( ( K e. AtLat /\ w C_ ( w u. v ) /\ ( w u. v ) C_ A ) -> ( U ` w ) C_ ( U ` ( w u. v ) ) )
65 54 63 58 64 syl3anc 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( U ` w ) C_ ( U ` ( w u. v ) ) )
66 simp2l 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> p e. ( U ` w ) )
67 65 66 sseldd 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> p e. ( U ` ( w u. v ) ) )
68 ssun2 
 |-  v C_ ( w u. v )
69 68 a1i 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> v C_ ( w u. v ) )
70 1 2 pclssN 
 |-  ( ( K e. AtLat /\ v C_ ( w u. v ) /\ ( w u. v ) C_ A ) -> ( U ` v ) C_ ( U ` ( w u. v ) ) )
71 54 69 58 70 syl3anc 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> ( U ` v ) C_ ( U ` ( w u. v ) ) )
72 simp13 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> q e. ( U ` v ) )
73 71 72 sseldd 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> q e. ( U ` ( w u. v ) ) )
74 simp3r 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> r ( le ` K ) ( p ( join ` K ) q ) )
75 eqid 
 |-  ( le ` K ) = ( le ` K )
76 eqid 
 |-  ( join ` K ) = ( join ` K )
77 75 76 1 12 psubspi2N 
 |-  ( ( ( K e. AtLat /\ ( U ` ( w u. v ) ) e. ( PSubSp ` K ) /\ r e. A ) /\ ( p e. ( U ` ( w u. v ) ) /\ q e. ( U ` ( w u. v ) ) /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> r e. ( U ` ( w u. v ) ) )
78 54 60 61 67 73 74 77 syl33anc 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> r e. ( U ` ( w u. v ) ) )
79 fveq2 
 |-  ( y = ( w u. v ) -> ( U ` y ) = ( U ` ( w u. v ) ) )
80 79 eleq2d 
 |-  ( y = ( w u. v ) -> ( r e. ( U ` y ) <-> r e. ( U ` ( w u. v ) ) ) )
81 80 rspcev 
 |-  ( ( ( w u. v ) e. ( Fin i^i ~P X ) /\ r e. ( U ` ( w u. v ) ) ) -> E. y e. ( Fin i^i ~P X ) r e. ( U ` y ) )
82 53 78 81 syl2anc 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> E. y e. ( Fin i^i ~P X ) r e. ( U ` y ) )
83 eliun 
 |-  ( r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) r e. ( U ` y ) )
84 82 83 sylibr 
 |-  ( ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) /\ ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) /\ ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) )
85 84 3exp 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) -> ( ( p e. ( U ` w ) /\ ( w e. Fin /\ w C_ X ) ) -> ( ( r e. A /\ r ( le ` K ) ( p ( join ` K ) q ) ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) )
86 85 exp5c 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ ( v e. Fin /\ v C_ X ) /\ q e. ( U ` v ) ) -> ( p e. ( U ` w ) -> ( ( w e. Fin /\ w C_ X ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) ) )
87 86 3exp 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( ( v e. Fin /\ v C_ X ) -> ( q e. ( U ` v ) -> ( p e. ( U ` w ) -> ( ( w e. Fin /\ w C_ X ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) ) ) ) )
88 40 87 syl5 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( v e. ( Fin i^i ~P X ) -> ( q e. ( U ` v ) -> ( p e. ( U ` w ) -> ( ( w e. Fin /\ w C_ X ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) ) ) ) )
89 88 rexlimdv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) -> ( p e. ( U ` w ) -> ( ( w e. Fin /\ w C_ X ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) ) ) )
90 89 com24 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( ( w e. Fin /\ w C_ X ) -> ( p e. ( U ` w ) -> ( E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) ) ) )
91 36 90 syl5 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( w e. ( Fin i^i ~P X ) -> ( p e. ( U ` w ) -> ( E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) ) ) )
92 91 rexlimdv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( E. w e. ( Fin i^i ~P X ) p e. ( U ` w ) -> ( E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) ) )
93 92 impd 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( ( E. w e. ( Fin i^i ~P X ) p e. ( U ` w ) /\ E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) )
94 32 93 biimtrid 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( ( p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) /\ q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) )
95 94 ralrimdv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( ( p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) /\ q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) -> A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) )
96 95 ralrimivv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> A. p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) A. q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) )
97 75 76 1 12 ispsubsp 
 |-  ( K e. AtLat -> ( U_ y e. ( Fin i^i ~P X ) ( U ` y ) e. ( PSubSp ` K ) <-> ( U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ A /\ A. p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) A. q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) )
98 97 adantr 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( U_ y e. ( Fin i^i ~P X ) ( U ` y ) e. ( PSubSp ` K ) <-> ( U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ A /\ A. p e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) A. q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) ) )
99 21 96 98 mpbir2and 
 |-  ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) e. ( PSubSp ` K ) )
100 snfi 
 |-  { w } e. Fin
101 100 a1i 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. Fin )
102 snelpwi 
 |-  ( w e. X -> { w } e. ~P X )
103 102 adantl 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. ~P X )
104 101 103 elind 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. ( Fin i^i ~P X ) )
105 vsnid 
 |-  w e. { w }
106 simpll 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> K e. AtLat )
107 ssel2 
 |-  ( ( X C_ A /\ w e. X ) -> w e. A )
108 107 adantll 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> w e. A )
109 1 12 snatpsubN 
 |-  ( ( K e. AtLat /\ w e. A ) -> { w } e. ( PSubSp ` K ) )
110 106 108 109 syl2anc 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. ( PSubSp ` K ) )
111 12 2 pclidN 
 |-  ( ( K e. AtLat /\ { w } e. ( PSubSp ` K ) ) -> ( U ` { w } ) = { w } )
112 106 110 111 syl2anc 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> ( U ` { w } ) = { w } )
113 105 112 eleqtrrid 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> w e. ( U ` { w } ) )
114 fveq2 
 |-  ( y = { w } -> ( U ` y ) = ( U ` { w } ) )
115 114 eleq2d 
 |-  ( y = { w } -> ( w e. ( U ` y ) <-> w e. ( U ` { w } ) ) )
116 115 rspcev 
 |-  ( ( { w } e. ( Fin i^i ~P X ) /\ w e. ( U ` { w } ) ) -> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) )
117 104 113 116 syl2anc 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) )
118 117 ex 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( w e. X -> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) ) )
119 eliun 
 |-  ( w e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) )
120 118 119 imbitrrdi 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( w e. X -> w e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) )
121 120 ssrdv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> X C_ U_ y e. ( Fin i^i ~P X ) ( U ` y ) )
122 simpr 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> y C_ X )
123 simplr 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> X C_ A )
124 1 2 pclssN 
 |-  ( ( K e. AtLat /\ y C_ X /\ X C_ A ) -> ( U ` y ) C_ ( U ` X ) )
125 8 122 123 124 syl3anc 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( U ` y ) C_ ( U ` X ) )
126 125 sseld 
 |-  ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( w e. ( U ` y ) -> w e. ( U ` X ) ) )
127 126 ex 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( y C_ X -> ( w e. ( U ` y ) -> w e. ( U ` X ) ) ) )
128 7 127 syl5 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( y e. ( Fin i^i ~P X ) -> ( w e. ( U ` y ) -> w e. ( U ` X ) ) ) )
129 128 rexlimdv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) -> w e. ( U ` X ) ) )
130 119 129 biimtrid 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( w e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) -> w e. ( U ` X ) ) )
131 130 ssrdv 
 |-  ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ ( U ` X ) )
132 12 2 pclbtwnN 
 |-  ( ( ( K e. AtLat /\ U_ y e. ( Fin i^i ~P X ) ( U ` y ) e. ( PSubSp ` K ) ) /\ ( X C_ U_ y e. ( Fin i^i ~P X ) ( U ` y ) /\ U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ ( U ` X ) ) ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) = ( U ` X ) )
133 3 99 121 131 132 syl22anc 
 |-  ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) = ( U ` X ) )
134 133 eqcomd 
 |-  ( ( K e. AtLat /\ X C_ A ) -> ( U ` X ) = U_ y e. ( Fin i^i ~P X ) ( U ` y ) )