Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  doca2N Unicode version

Theorem doca2N 31134
Description: Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
doca2.h  |-  H  =  ( LHyp `  K
)
doca2.i  |-  I  =  ( ( DIsoA `  K
) `  W )
doca2.n  |-  ._|_  =  ( ( ocA `  K
) `  W )
Assertion
Ref Expression
doca2N  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (  ._|_  `  (  ._|_  `  (
I `  X )
) )  =  ( I `  X ) )

Proof of Theorem doca2N
StepHypRef Expression
1 hlol 29369 . . . . . . . . . . . . 13  |-  ( K  e.  HL  ->  K  e.  OL )
21ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  K  e.  OL )
3 eqid 2316 . . . . . . . . . . . . 13  |-  ( Base `  K )  =  (
Base `  K )
4 doca2.h . . . . . . . . . . . . 13  |-  H  =  ( LHyp `  K
)
5 doca2.i . . . . . . . . . . . . 13  |-  I  =  ( ( DIsoA `  K
) `  W )
63, 4, 5diadmclN 31045 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  X  e.  ( Base `  K
) )
73, 4lhpbase 30005 . . . . . . . . . . . . 13  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
87ad2antlr 707 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  W  e.  ( Base `  K
) )
9 eqid 2316 . . . . . . . . . . . . 13  |-  ( join `  K )  =  (
join `  K )
10 eqid 2316 . . . . . . . . . . . . 13  |-  ( meet `  K )  =  (
meet `  K )
11 eqid 2316 . . . . . . . . . . . . 13  |-  ( oc
`  K )  =  ( oc `  K
)
123, 9, 10, 11oldmm1 29225 . . . . . . . . . . . 12  |-  ( ( K  e.  OL  /\  X  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  (
( oc `  K
) `  ( X
( meet `  K ) W ) )  =  ( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
132, 6, 8, 12syl3anc 1182 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( oc `  K
) `  ( X
( meet `  K ) W ) )  =  ( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
1413oveq1d 5915 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( oc `  K ) `  ( X ( meet `  K
) W ) ) ( meet `  K
) W )  =  ( ( ( ( oc `  K ) `
 X ) (
join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )
1514eqcomd 2321 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W )  =  ( ( ( oc
`  K ) `  ( X ( meet `  K
) W ) ) ( meet `  K
) W ) )
1615fveq2d 5567 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( oc `  K
) `  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) )  =  ( ( oc `  K ) `  (
( ( oc `  K ) `  ( X ( meet `  K
) W ) ) ( meet `  K
) W ) ) )
17 hllat 29371 . . . . . . . . . . 11  |-  ( K  e.  HL  ->  K  e.  Lat )
1817ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  K  e.  Lat )
193, 10latmcl 14206 . . . . . . . . . 10  |-  ( ( K  e.  Lat  /\  X  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  ( X ( meet `  K
) W )  e.  ( Base `  K
) )
2018, 6, 8, 19syl3anc 1182 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  ( X ( meet `  K
) W )  e.  ( Base `  K
) )
213, 9, 10, 11oldmm2 29226 . . . . . . . . 9  |-  ( ( K  e.  OL  /\  ( X ( meet `  K
) W )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( oc `  K ) `  ( ( ( oc
`  K ) `  ( X ( meet `  K
) W ) ) ( meet `  K
) W ) )  =  ( ( X ( meet `  K
) W ) (
join `  K )
( ( oc `  K ) `  W
) ) )
222, 20, 8, 21syl3anc 1182 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( oc `  K
) `  ( (
( oc `  K
) `  ( X
( meet `  K ) W ) ) (
meet `  K ) W ) )  =  ( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
2316, 22eqtrd 2348 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( oc `  K
) `  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) )  =  ( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
2423oveq1d 5915 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( oc `  K ) `  (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) )  =  ( ( ( X ( meet `  K
) W ) (
join `  K )
( ( oc `  K ) `  W
) ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
25 hlop 29370 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  OP )
2625ad2antrr 706 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  K  e.  OP )
273, 11opoccl 29202 . . . . . . . . 9  |-  ( ( K  e.  OP  /\  W  e.  ( Base `  K ) )  -> 
( ( oc `  K ) `  W
)  e.  ( Base `  K ) )
2826, 8, 27syl2anc 642 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( oc `  K
) `  W )  e.  ( Base `  K
) )
293, 9latjass 14250 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( ( X (
meet `  K ) W )  e.  (
Base `  K )  /\  ( ( oc `  K ) `  W
)  e.  ( Base `  K )  /\  (
( oc `  K
) `  W )  e.  ( Base `  K
) ) )  -> 
( ( ( X ( meet `  K
) W ) (
join `  K )
( ( oc `  K ) `  W
) ) ( join `  K ) ( ( oc `  K ) `
 W ) )  =  ( ( X ( meet `  K
) W ) (
join `  K )
( ( ( oc
`  K ) `  W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ) )
3018, 20, 28, 28, 29syl13anc 1184 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) )  =  ( ( X (
meet `  K ) W ) ( join `  K ) ( ( ( oc `  K
) `  W )
( join `  K )
( ( oc `  K ) `  W
) ) ) )
313, 9latjidm 14229 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  W
)  e.  ( Base `  K ) )  -> 
( ( ( oc
`  K ) `  W ) ( join `  K ) ( ( oc `  K ) `
 W ) )  =  ( ( oc
`  K ) `  W ) )
3218, 28, 31syl2anc 642 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( oc `  K ) `  W
) ( join `  K
) ( ( oc
`  K ) `  W ) )  =  ( ( oc `  K ) `  W
) )
3332oveq2d 5916 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( X ( meet `  K ) W ) ( join `  K
) ( ( ( oc `  K ) `
 W ) (
join `  K )
( ( oc `  K ) `  W
) ) )  =  ( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
3430, 33eqtrd 2348 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) )  =  ( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
3524, 34eqtrd 2348 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( oc `  K ) `  (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) )  =  ( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) )
3635oveq1d 5915 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( ( oc
`  K ) `  ( ( ( ( oc `  K ) `
 X ) (
join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W )  =  ( ( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W ) )
37 hloml 29365 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  OML )
3837ad2antrr 706 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  K  e.  OML )
39 eqid 2316 . . . . . . 7  |-  ( le
`  K )  =  ( le `  K
)
403, 39, 10latmle2 14232 . . . . . 6  |-  ( ( K  e.  Lat  /\  X  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  ( X ( meet `  K
) W ) ( le `  K ) W )
4118, 6, 8, 40syl3anc 1182 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  ( X ( meet `  K
) W ) ( le `  K ) W )
423, 39, 9, 10, 11omlspjN 29269 . . . . 5  |-  ( ( K  e.  OML  /\  ( ( X (
meet `  K ) W )  e.  (
Base `  K )  /\  W  e.  ( Base `  K ) )  /\  ( X (
meet `  K ) W ) ( le
`  K ) W )  ->  ( (
( X ( meet `  K ) W ) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W )  =  ( X ( meet `  K
) W ) )
4338, 20, 8, 41, 42syl121anc 1187 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( X (
meet `  K ) W ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W )  =  ( X ( meet `  K ) W ) )
4439, 4, 5diadmleN 31046 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  X
( le `  K
) W )
453, 39, 10latleeqm1 14234 . . . . . 6  |-  ( ( K  e.  Lat  /\  X  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  ( X ( le `  K ) W  <->  ( X
( meet `  K ) W )  =  X ) )
4618, 6, 8, 45syl3anc 1182 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  ( X ( le `  K ) W  <->  ( X
( meet `  K ) W )  =  X ) )
4744, 46mpbid 201 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  ( X ( meet `  K
) W )  =  X )
4836, 43, 473eqtrrd 2353 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  X  =  ( ( ( ( oc `  K
) `  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) ) (
join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )
4948fveq2d 5567 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
I `  X )  =  ( I `  ( ( ( ( oc `  K ) `
 ( ( ( ( oc `  K
) `  X )
( join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) ) )
503, 11opoccl 29202 . . . . . . 7  |-  ( ( K  e.  OP  /\  X  e.  ( Base `  K ) )  -> 
( ( oc `  K ) `  X
)  e.  ( Base `  K ) )
5126, 6, 50syl2anc 642 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( oc `  K
) `  X )  e.  ( Base `  K
) )
523, 9latjcl 14205 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  X
)  e.  ( Base `  K )  /\  (
( oc `  K
) `  W )  e.  ( Base `  K
) )  ->  (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) )  e.  ( Base `  K
) )
5318, 51, 28, 52syl3anc 1182 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) )  e.  ( Base `  K
) )
543, 10latmcl 14206 . . . . 5  |-  ( ( K  e.  Lat  /\  ( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W )  e.  (
Base `  K )
)
5518, 53, 8, 54syl3anc 1182 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W )  e.  ( Base `  K
) )
563, 39, 10latmle2 14232 . . . . 5  |-  ( ( K  e.  Lat  /\  ( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) ( le
`  K ) W )
5718, 53, 8, 56syl3anc 1182 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W ) ( le `  K ) W )
583, 39, 4, 5diaeldm 31044 . . . . 5  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( ( ( ( oc `  K
) `  X )
( join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I  <->  ( (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) ( le
`  K ) W ) ) )
5958adantr 451 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( ( ( oc `  K ) `
 X ) (
join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I  <->  ( (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) ( le
`  K ) W ) ) )
6055, 57, 59mpbir2and 888 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W )  e. 
dom  I )
61 eqid 2316 . . . 4  |-  ( (
LTrn `  K ) `  W )  =  ( ( LTrn `  K
) `  W )
62 doca2.n . . . 4  |-  ._|_  =  ( ( ocA `  K
) `  W )
639, 10, 11, 4, 61, 5, 62diaocN 31133 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( ( ( oc `  K
) `  X )
( join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I )  ->  ( I `  ( ( ( ( oc `  K ) `
 ( ( ( ( oc `  K
) `  X )
( join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) )  =  (  ._|_  `  ( I `
 ( ( ( ( oc `  K
) `  X )
( join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) )
6460, 63syldan 456 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
I `  ( (
( ( oc `  K ) `  (
( ( ( oc
`  K ) `  X ) ( join `  K ) ( ( oc `  K ) `
 W ) ) ( meet `  K
) W ) ) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) )  =  (  ._|_  `  ( I `
 ( ( ( ( oc `  K
) `  X )
( join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) )
659, 10, 11, 4, 61, 5, 62diaocN 31133 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
I `  ( (
( ( oc `  K ) `  X
) ( join `  K
) ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) )  =  (  ._|_  `  ( I `
 X ) ) )
6665fveq2d 5567 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (  ._|_  `  ( I `  ( ( ( ( oc `  K ) `
 X ) (
join `  K )
( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  =  ( 
._|_  `  (  ._|_  `  (
I `  X )
) ) )
6749, 64, 663eqtrrd 2353 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (  ._|_  `  (  ._|_  `  (
I `  X )
) )  =  ( I `  X ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1633    e. wcel 1701   class class class wbr 4060   dom cdm 4726   ` cfv 5292  (class class class)co 5900   Basecbs 13195   lecple 13262   occoc 13263   joincjn 14127   meetcmee 14128   Latclat 14200   OPcops 29180   OLcol 29182   OMLcoml 29183   HLchlt 29358   LHypclh 29991   LTrncltrn 30108   DIsoAcdia 31036   ocAcocaN 31127
This theorem is referenced by:  doca3N  31135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-iin 3945  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-undef 6340  df-riota 6346  df-map 6817  df-poset 14129  df-plt 14141  df-lub 14157  df-glb 14158  df-join 14159  df-meet 14160  df-p0 14194  df-p1 14195  df-lat 14201  df-clat 14263  df-oposet 29184  df-cmtN 29185  df-ol 29186  df-oml 29187  df-covers 29274  df-ats 29275  df-atl 29306  df-cvlat 29330  df-hlat 29359  df-llines 29505  df-lplanes 29506  df-lvols 29507  df-lines 29508  df-psubsp 29510  df-pmap 29511  df-padd 29803  df-lhyp 29995  df-laut 29996  df-ldil 30111  df-ltrn 30112  df-trl 30166  df-disoa 31037  df-docaN 31128
  Copyright terms: Public domain W3C validator