Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pclfinN Structured version   Visualization version   Unicode version
Theorem pclfinN 35186
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 35236. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
pclfin.a |- A = ( Atoms ` K )
pclfin.c |- U = ( PCl ` K )
Assertion
Ref Expression
pclfinN |- ( ( K e. AtLat /\ X C_ A ) -> ( U ` X ) = U_ y e. ( Fin i^i ~P X ) ( U ` y ) )
Distinct variable groups:   y, A   y, U   y, K   y, X
Proof of Theorem pclfinN
Dummy variables q p r v w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 473 . . 3 |- ( ( K e. AtLat /\ X C_ A ) -> K e. AtLat )
2 elin 3796 . . . . . . . 8 |- ( y e. ( Fin i^i ~P X ) <-> ( y e. Fin /\ y e. ~P X ) )
3 elpwi 4168 . . . . . . . . 9 |- ( y e. ~P X -> y C_ X )
43adantl 482 . . . . . . . 8 |- ( ( y e. Fin /\ y e. ~P X ) -> y C_ X )
52, 4sylbi 207 . . . . . . 7 |- ( y e. ( Fin i^i ~P X ) -> y C_ X )
6 simpll 790 . . . . . . . . 9 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> K e. AtLat )
7 sstr 3611 . . . . . . . . . . . 12 |- ( ( y C_ X /\ X C_ A ) -> y C_ A )
87ancoms 469 . . . . . . . . . . 11 |- ( ( X C_ A /\ y C_ X ) -> y C_ A )
98adantll 750 . . . . . . . . . 10 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> y C_ A )
10 pclfin.a . . . . . . . . . . 11 |- A = ( Atoms ` K )
11 eqid 2622 . . . . . . . . . . 11 |- ( PSubSp ` K ) = ( PSubSp ` K )
12 pclfin.c . . . . . . . . . . 11 |- U = ( PCl ` K )
1310, 11, 12pclclN 35177 . . . . . . . . . 10 |- ( ( K e. AtLat /\ y C_ A ) -> ( U ` y ) e. ( PSubSp ` K ) )
146, 9, 13syl2anc 693 . . . . . . . . 9 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( U ` y ) e. ( PSubSp ` K ) )
1510, 11psubssat 35040 . . . . . . . . 9 |- ( ( K e. AtLat /\ ( U ` y ) e. ( PSubSp ` K ) ) -> ( U ` y ) C_ A )
166, 14, 15syl2anc 693 . . . . . . . 8 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( U ` y ) C_ A )
1716ex 450 . . . . . . 7 |- ( ( K e. AtLat /\ X C_ A ) -> ( y C_ X -> ( U ` y ) C_ A ) )
185, 17syl5 34 . . . . . 6 |- ( ( K e. AtLat /\ X C_ A ) -> ( y e. ( Fin i^i ~P X ) -> ( U ` y ) C_ A ) )
1918ralrimiv 2965 . . . . 5 |- ( ( K e. AtLat /\ X C_ A ) -> A. y e. ( Fin i^i ~P X ) ( U ` y ) C_ A )
20 iunss 4561 . . . . 5 |- ( U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ A <-> A. y e. ( Fin i^i ~P X ) ( U ` y ) C_ A )
2119, 20sylibr 224 . . . 4 |- ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ A )
22 eliun 4524 . . . . . . . . 9 |- ( 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 6191 . . . . . . . . . . 11 |- ( y = w -> ( U ` y ) = ( U ` w ) )
2423eleq2d 2687 . . . . . . . . . 10 |- ( y = w -> ( p e. ( U ` y ) <-> p e. ( U ` w ) ) )
2524cbvrexv 3172 . . . . . . . . 9 |- ( E. y e. ( Fin i^i ~P X ) p e. ( U ` y ) <-> E. w e. ( Fin i^i ~P X ) p e. ( U ` w ) )
2622, 25bitri 264 . . . . . . . 8 |- ( 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 4524 . . . . . . . . 9 |- ( 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 6191 . . . . . . . . . . 11 |- ( y = v -> ( U ` y ) = ( U ` v ) )
2928eleq2d 2687 . . . . . . . . . 10 |- ( y = v -> ( q e. ( U ` y ) <-> q e. ( U ` v ) ) )
3029cbvrexv 3172 . . . . . . . . 9 |- ( E. y e. ( Fin i^i ~P X ) q e. ( U ` y ) <-> E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) )
3127, 30bitri 264 . . . . . . . 8 |- ( q e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. v e. ( Fin i^i ~P X ) q e. ( U ` v ) )
3226, 31anbi12i 733 . . . . . . 7 |- ( ( 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 3796 . . . . . . . . . . 11 |- ( w e. ( Fin i^i ~P X ) <-> ( w e. Fin /\ w e. ~P X ) )
34 elpwi 4168 . . . . . . . . . . . 12 |- ( w e. ~P X -> w C_ X )
3534anim2i 593 . . . . . . . . . . 11 |- ( ( w e. Fin /\ w e. ~P X ) -> ( w e. Fin /\ w C_ X ) )
3633, 35sylbi 207 . . . . . . . . . 10 |- ( w e. ( Fin i^i ~P X ) -> ( w e. Fin /\ w C_ X ) )
37 elin 3796 . . . . . . . . . . . . . 14 |- ( v e. ( Fin i^i ~P X ) <-> ( v e. Fin /\ v e. ~P X ) )
38 elpwi 4168 . . . . . . . . . . . . . . 15 |- ( v e. ~P X -> v C_ X )
3938anim2i 593 . . . . . . . . . . . . . 14 |- ( ( v e. Fin /\ v e. ~P X ) -> ( v e. Fin /\ v C_ X ) )
4037, 39sylbi 207 . . . . . . . . . . . . 13 |- ( v e. ( Fin i^i ~P X ) -> ( v e. Fin /\ v C_ X ) )
41 simp2rl 1130 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 1174 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 8227 . . . . . . . . . . . . . . . . . . . 20 |- ( ( w e. Fin /\ v e. Fin ) -> ( w u. v ) e. Fin )
4441, 42, 43syl2anc 693 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 1131 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 1175 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 )
4745, 46unssd 3789 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 3203 . . . . . . . . . . . . . . . . . . . . . 22 |- w e. _V
49 vex 3203 . . . . . . . . . . . . . . . . . . . . . 22 |- v e. _V
5048, 49unex 6956 . . . . . . . . . . . . . . . . . . . . 21 |- ( w u. v ) e. _V
5150elpw 4164 . . . . . . . . . . . . . . . . . . . 20 |- ( ( w u. v ) e. ~P X <-> ( w u. v ) C_ X )
5247, 51sylibr 224 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
5344, 52elind 3798 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 1172 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 1173 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 )
5645, 55sstrd 3613 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 )
5746, 55sstrd 3613 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 )
5856, 57unssd 3789 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 )
5910, 11, 12pclclN 35177 . . . . . . . . . . . . . . . . . . . 20 |- ( ( K e. AtLat /\ ( w u. v ) C_ A ) -> ( U ` ( w u. v ) ) e. ( PSubSp ` K ) )
6054, 58, 59syl2anc 693 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 1089 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 3776 . . . . . . . . . . . . . . . . . . . . . 22 |- w C_ ( w u. v )
6362a1i 11 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) )
6410, 12pclssN 35180 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( K e. AtLat /\ w C_ ( w u. v ) /\ ( w u. v ) C_ A ) -> ( U ` w ) C_ ( U ` ( w u. v ) ) )
6554, 63, 58, 64syl3anc 1326 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 1087 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) )
6765, 66sseldd 3604 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 3777 . . . . . . . . . . . . . . . . . . . . . 22 |- v C_ ( w u. v )
6968a1i 11 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) )
7010, 12pclssN 35180 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( K e. AtLat /\ v C_ ( w u. v ) /\ ( w u. v ) C_ A ) -> ( U ` v ) C_ ( U ` ( w u. v ) ) )
7154, 69, 58, 70syl3anc 1326 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 1093 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) )
7371, 72sseldd 3604 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 1090 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 2622 . . . . . . . . . . . . . . . . . . . 20 |- ( le ` K ) = ( le ` K )
76 eqid 2622 . . . . . . . . . . . . . . . . . . . 20 |- ( join ` K ) = ( join ` K )
7775, 76, 10, 11psubspi2N 35034 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) )
7854, 60, 61, 67, 73, 74, 77syl33anc 1341 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 6191 . . . . . . . . . . . . . . . . . . . 20 |- ( y = ( w u. v ) -> ( U ` y ) = ( U ` ( w u. v ) ) )
8079eleq2d 2687 . . . . . . . . . . . . . . . . . . 19 |- ( y = ( w u. v ) -> ( r e. ( U ` y ) <-> r e. ( U ` ( w u. v ) ) ) )
8180rspcev 3309 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
8253, 78, 81syl2anc 693 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 4524 . . . . . . . . . . . . . . . . 17 |- ( r e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) r e. ( U ` y ) )
8482, 83sylibr 224 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
85843exp 1264 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
8685exp5c 644 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) ) ) )
87863exp 1264 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) ) ) ) ) )
8840, 87syl5 34 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) ) ) ) ) )
8988rexlimdv 3030 . . . . . . . . . . 11 |- ( ( 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 ) ) ) ) ) ) )
9089com24 95 . . . . . . . . . 10 |- ( ( 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 ) ) ) ) ) ) )
9136, 90syl5 34 . . . . . . . . 9 |- ( ( 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 ) ) ) ) ) ) )
9291rexlimdv 3030 . . . . . . . 8 |- ( ( 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 ) ) ) ) ) )
9392impd 447 . . . . . . 7 |- ( ( 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 ) ) ) ) )
9432, 93syl5bi 232 . . . . . 6 |- ( ( 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 ) ) ) ) )
9594ralrimdv 2968 . . . . 5 |- ( ( 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 ) ) ) )
9695ralrimivv 2970 . . . 4 |- ( ( 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 ) ) )
9775, 76, 10, 11ispsubsp 35031 . . . . 5 |- ( 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 ) ) ) ) )
9897adantr 481 . . . 4 |- ( ( 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 ) ) ) ) )
9921, 96, 98mpbir2and 957 . . 3 |- ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) e. ( PSubSp ` K ) )
100 snfi 8038 . . . . . . . . 9 |- { w } e. Fin
101100a1i 11 . . . . . . . 8 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. Fin )
102 snelpwi 4912 . . . . . . . . 9 |- ( w e. X -> { w } e. ~P X )
103102adantl 482 . . . . . . . 8 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. ~P X )
104101, 103elind 3798 . . . . . . 7 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. ( Fin i^i ~P X ) )
105 vsnid 4209 . . . . . . . 8 |- w e. { w }
106 simpll 790 . . . . . . . . 9 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> K e. AtLat )
107 ssel2 3598 . . . . . . . . . . 11 |- ( ( X C_ A /\ w e. X ) -> w e. A )
108107adantll 750 . . . . . . . . . 10 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> w e. A )
10910, 11snatpsubN 35036 . . . . . . . . . 10 |- ( ( K e. AtLat /\ w e. A ) -> { w } e. ( PSubSp ` K ) )
110106, 108, 109syl2anc 693 . . . . . . . . 9 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> { w } e. ( PSubSp ` K ) )
11111, 12pclidN 35182 . . . . . . . . 9 |- ( ( K e. AtLat /\ { w } e. ( PSubSp ` K ) ) -> ( U ` { w } ) = { w } )
112106, 110, 111syl2anc 693 . . . . . . . 8 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> ( U ` { w } ) = { w } )
113105, 112syl5eleqr 2708 . . . . . . 7 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> w e. ( U ` { w } ) )
114 fveq2 6191 . . . . . . . . 9 |- ( y = { w } -> ( U ` y ) = ( U ` { w } ) )
115114eleq2d 2687 . . . . . . . 8 |- ( y = { w } -> ( w e. ( U ` y ) <-> w e. ( U ` { w } ) ) )
116115rspcev 3309 . . . . . . 7 |- ( ( { w } e. ( Fin i^i ~P X ) /\ w e. ( U ` { w } ) ) -> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) )
117104, 113, 116syl2anc 693 . . . . . 6 |- ( ( ( K e. AtLat /\ X C_ A ) /\ w e. X ) -> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) )
118117ex 450 . . . . 5 |- ( ( K e. AtLat /\ X C_ A ) -> ( w e. X -> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) ) )
119 eliun 4524 . . . . 5 |- ( w e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) )
120118, 119syl6ibr 242 . . . 4 |- ( ( K e. AtLat /\ X C_ A ) -> ( w e. X -> w e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) )
121120ssrdv 3609 . . 3 |- ( ( K e. AtLat /\ X C_ A ) -> X C_ U_ y e. ( Fin i^i ~P X ) ( U ` y ) )
122 simpr 477 . . . . . . . . . 10 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> y C_ X )
123 simplr 792 . . . . . . . . . 10 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> X C_ A )
12410, 12pclssN 35180 . . . . . . . . . 10 |- ( ( K e. AtLat /\ y C_ X /\ X C_ A ) -> ( U ` y ) C_ ( U ` X ) )
1256, 122, 123, 124syl3anc 1326 . . . . . . . . 9 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( U ` y ) C_ ( U ` X ) )
126125sseld 3602 . . . . . . . 8 |- ( ( ( K e. AtLat /\ X C_ A ) /\ y C_ X ) -> ( w e. ( U ` y ) -> w e. ( U ` X ) ) )
127126ex 450 . . . . . . 7 |- ( ( K e. AtLat /\ X C_ A ) -> ( y C_ X -> ( w e. ( U ` y ) -> w e. ( U ` X ) ) ) )
1285, 127syl5 34 . . . . . 6 |- ( ( K e. AtLat /\ X C_ A ) -> ( y e. ( Fin i^i ~P X ) -> ( w e. ( U ` y ) -> w e. ( U ` X ) ) ) )
129128rexlimdv 3030 . . . . 5 |- ( ( K e. AtLat /\ X C_ A ) -> ( E. y e. ( Fin i^i ~P X ) w e. ( U ` y ) -> w e. ( U ` X ) ) )
130119, 129syl5bi 232 . . . 4 |- ( ( K e. AtLat /\ X C_ A ) -> ( w e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) -> w e. ( U ` X ) ) )
131130ssrdv 3609 . . 3 |- ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) C_ ( U ` X ) )
13211, 12pclbtwnN 35183 . . 3 |- ( ( ( 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 ) )
1331, 99, 121, 131, 132syl22anc 1327 . 2 |- ( ( K e. AtLat /\ X C_ A ) -> U_ y e. ( Fin i^i ~P X ) ( U ` y ) = ( U ` X ) )
134133eqcomd 2628 1 |- ( ( K e. AtLat /\ X C_ A ) -> ( U ` X ) = U_ y e. ( Fin i^i ~P X ) ( U ` y ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   u. cun 3572   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   {csn 4177   U_ciun 4520   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   Fincfn 7955   lecple 15948   joincjn 16944   Atomscatm 34550   AtLatcal 34551   PSubSpcpsubsp 34782   PClcpclN 35173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-fin 7959  df-preset 16928  df-poset 16946  df-plt 16958  df-lub 16974  df-glb 16975  df-join 16976  df-meet 16977  df-p0 17039  df-lat 17046  df-covers 34553  df-ats 34554  df-atl 34585  df-psubsp 34789  df-pclN 35174
This theorem is referenced by:  pclcmpatN  35187
  Copyright terms: Public domain W3C validator