Metamath Proof Explorer

Theorem glbconxN

Description: De Morgan's law for GLB and LUB. Index-set version of glbconN , where we read S as S ( i ) . (Contributed by NM, 17-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses glbcon.b 
|- B = ( Base ` K )
glbcon.u 
|- U = ( lub ` K )
glbcon.g 
|- G = ( glb ` K )
glbcon.o 
|- ._|_ = ( oc ` K )
Assertion glbconxN 
|- ( ( K e. HL /\ A. i e. I S e. B ) -> ( G ` { x | E. i e. I x = S } ) = ( ._|_ ` ( U ` { x | E. i e. I x = ( ._|_ ` S ) } ) ) )

Proof

Step Hyp Ref Expression
1 glbcon.b 
 |-  B = ( Base ` K )
2 glbcon.u 
 |-  U = ( lub ` K )
3 glbcon.g 
 |-  G = ( glb ` K )
4 glbcon.o 
 |-  ._|_ = ( oc ` K )
5 vex 
 |-  y e. _V
6 eqeq1 
 |-  ( x = y -> ( x = S <-> y = S ) )
7 6 rexbidv 
 |-  ( x = y -> ( E. i e. I x = S <-> E. i e. I y = S ) )
8 5 7 elab 
 |-  ( y e. { x | E. i e. I x = S } <-> E. i e. I y = S )
9 nfra1 
 |-  F/ i A. i e. I S e. B
10 nfv 
 |-  F/ i y e. B
11 rsp 
 |-  ( A. i e. I S e. B -> ( i e. I -> S e. B ) )
12 eleq1a 
 |-  ( S e. B -> ( y = S -> y e. B ) )
13 11 12 syl6 
 |-  ( A. i e. I S e. B -> ( i e. I -> ( y = S -> y e. B ) ) )
14 9 10 13 rexlimd 
 |-  ( A. i e. I S e. B -> ( E. i e. I y = S -> y e. B ) )
15 8 14 syl5bi 
 |-  ( A. i e. I S e. B -> ( y e. { x | E. i e. I x = S } -> y e. B ) )
16 15 ssrdv 
 |-  ( A. i e. I S e. B -> { x | E. i e. I x = S } C_ B )
17 1 2 3 4 glbconN 
 |-  ( ( K e. HL /\ { x | E. i e. I x = S } C_ B ) -> ( G ` { x | E. i e. I x = S } ) = ( ._|_ ` ( U ` { y e. B | ( ._|_ ` y ) e. { x | E. i e. I x = S } } ) ) )
18 16 17 sylan2 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( G ` { x | E. i e. I x = S } ) = ( ._|_ ` ( U ` { y e. B | ( ._|_ ` y ) e. { x | E. i e. I x = S } } ) ) )
19 fvex 
 |-  ( ._|_ ` y ) e. _V
20 eqeq1 
 |-  ( x = ( ._|_ ` y ) -> ( x = S <-> ( ._|_ ` y ) = S ) )
21 20 rexbidv 
 |-  ( x = ( ._|_ ` y ) -> ( E. i e. I x = S <-> E. i e. I ( ._|_ ` y ) = S ) )
22 19 21 elab 
 |-  ( ( ._|_ ` y ) e. { x | E. i e. I x = S } <-> E. i e. I ( ._|_ ` y ) = S )
23 22 rabbii 
 |-  { y e. B | ( ._|_ ` y ) e. { x | E. i e. I x = S } } = { y e. B | E. i e. I ( ._|_ ` y ) = S }
24 df-rab 
 |-  { y e. B | E. i e. I ( ._|_ ` y ) = S } = { y | ( y e. B /\ E. i e. I ( ._|_ ` y ) = S ) }
25 23 24 eqtri 
 |-  { y e. B | ( ._|_ ` y ) e. { x | E. i e. I x = S } } = { y | ( y e. B /\ E. i e. I ( ._|_ ` y ) = S ) }
26 nfv 
 |-  F/ i K e. HL
27 26 9 nfan 
 |-  F/ i ( K e. HL /\ A. i e. I S e. B )
28 rspa 
 |-  ( ( A. i e. I S e. B /\ i e. I ) -> S e. B )
29 hlop 
 |-  ( K e. HL -> K e. OP )
30 1 4 opoccl 
 |-  ( ( K e. OP /\ S e. B ) -> ( ._|_ ` S ) e. B )
31 29 30 sylan 
 |-  ( ( K e. HL /\ S e. B ) -> ( ._|_ ` S ) e. B )
32 eleq1a 
 |-  ( ( ._|_ ` S ) e. B -> ( y = ( ._|_ ` S ) -> y e. B ) )
33 31 32 syl 
 |-  ( ( K e. HL /\ S e. B ) -> ( y = ( ._|_ ` S ) -> y e. B ) )
34 33 pm4.71rd 
 |-  ( ( K e. HL /\ S e. B ) -> ( y = ( ._|_ ` S ) <-> ( y e. B /\ y = ( ._|_ ` S ) ) ) )
35 1 4 opcon2b 
 |-  ( ( K e. OP /\ S e. B /\ y e. B ) -> ( S = ( ._|_ ` y ) <-> y = ( ._|_ ` S ) ) )
36 29 35 syl3an1 
 |-  ( ( K e. HL /\ S e. B /\ y e. B ) -> ( S = ( ._|_ ` y ) <-> y = ( ._|_ ` S ) ) )
37 36 3expa 
 |-  ( ( ( K e. HL /\ S e. B ) /\ y e. B ) -> ( S = ( ._|_ ` y ) <-> y = ( ._|_ ` S ) ) )
38 eqcom 
 |-  ( S = ( ._|_ ` y ) <-> ( ._|_ ` y ) = S )
39 37 38 bitr3di 
 |-  ( ( ( K e. HL /\ S e. B ) /\ y e. B ) -> ( y = ( ._|_ ` S ) <-> ( ._|_ ` y ) = S ) )
40 39 pm5.32da 
 |-  ( ( K e. HL /\ S e. B ) -> ( ( y e. B /\ y = ( ._|_ ` S ) ) <-> ( y e. B /\ ( ._|_ ` y ) = S ) ) )
41 34 40 bitrd 
 |-  ( ( K e. HL /\ S e. B ) -> ( y = ( ._|_ ` S ) <-> ( y e. B /\ ( ._|_ ` y ) = S ) ) )
42 28 41 sylan2 
 |-  ( ( K e. HL /\ ( A. i e. I S e. B /\ i e. I ) ) -> ( y = ( ._|_ ` S ) <-> ( y e. B /\ ( ._|_ ` y ) = S ) ) )
43 42 anassrs 
 |-  ( ( ( K e. HL /\ A. i e. I S e. B ) /\ i e. I ) -> ( y = ( ._|_ ` S ) <-> ( y e. B /\ ( ._|_ ` y ) = S ) ) )
44 27 43 rexbida 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( E. i e. I y = ( ._|_ ` S ) <-> E. i e. I ( y e. B /\ ( ._|_ ` y ) = S ) ) )
45 r19.42v 
 |-  ( E. i e. I ( y e. B /\ ( ._|_ ` y ) = S ) <-> ( y e. B /\ E. i e. I ( ._|_ ` y ) = S ) )
46 44 45 bitr2di 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( ( y e. B /\ E. i e. I ( ._|_ ` y ) = S ) <-> E. i e. I y = ( ._|_ ` S ) ) )
47 46 abbidv 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> { y | ( y e. B /\ E. i e. I ( ._|_ ` y ) = S ) } = { y | E. i e. I y = ( ._|_ ` S ) } )
48 eqeq1 
 |-  ( y = x -> ( y = ( ._|_ ` S ) <-> x = ( ._|_ ` S ) ) )
49 48 rexbidv 
 |-  ( y = x -> ( E. i e. I y = ( ._|_ ` S ) <-> E. i e. I x = ( ._|_ ` S ) ) )
50 49 cbvabv 
 |-  { y | E. i e. I y = ( ._|_ ` S ) } = { x | E. i e. I x = ( ._|_ ` S ) }
51 47 50 eqtrdi 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> { y | ( y e. B /\ E. i e. I ( ._|_ ` y ) = S ) } = { x | E. i e. I x = ( ._|_ ` S ) } )
52 25 51 syl5eq 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> { y e. B | ( ._|_ ` y ) e. { x | E. i e. I x = S } } = { x | E. i e. I x = ( ._|_ ` S ) } )
53 52 fveq2d 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( U ` { y e. B | ( ._|_ ` y ) e. { x | E. i e. I x = S } } ) = ( U ` { x | E. i e. I x = ( ._|_ ` S ) } ) )
54 53 fveq2d 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( ._|_ ` ( U ` { y e. B | ( ._|_ ` y ) e. { x | E. i e. I x = S } } ) ) = ( ._|_ ` ( U ` { x | E. i e. I x = ( ._|_ ` S ) } ) ) )
55 18 54 eqtrd 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( G ` { x | E. i e. I x = S } ) = ( ._|_ ` ( U ` { x | E. i e. I x = ( ._|_ ` S ) } ) ) )