Metamath Proof Explorer

Theorem latlem

Description: Lemma for lattice properties. (Contributed by NM, 14-Sep-2011)

Ref Expression
Hypotheses latlem.b 
|- B = ( Base ` K )
latlem.j 
|- .\/ = ( join ` K )
latlem.m 
|- ./\ = ( meet ` K )
Assertion latlem 
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X .\/ Y ) e. B /\ ( X ./\ Y ) e. B ) )

Proof

Step Hyp Ref Expression
1 latlem.b 
 |-  B = ( Base ` K )
2 latlem.j 
 |-  .\/ = ( join ` K )
3 latlem.m 
 |-  ./\ = ( meet ` K )
4 simp1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Lat )
5 simp2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X e. B )
6 simp3 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y e. B )
7 opelxpi 
 |-  ( ( X e. B /\ Y e. B ) -> <. X , Y >. e. ( B X. B ) )
8 7 3adant1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> <. X , Y >. e. ( B X. B ) )
9 1 2 3 islat 
 |-  ( K e. Lat <-> ( K e. Poset /\ ( dom .\/ = ( B X. B ) /\ dom ./\ = ( B X. B ) ) ) )
10 simprl 
 |-  ( ( K e. Poset /\ ( dom .\/ = ( B X. B ) /\ dom ./\ = ( B X. B ) ) ) -> dom .\/ = ( B X. B ) )
11 9 10 sylbi 
 |-  ( K e. Lat -> dom .\/ = ( B X. B ) )
12 11 3ad2ant1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> dom .\/ = ( B X. B ) )
13 8 12 eleqtrrd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> <. X , Y >. e. dom .\/ )
14 1 2 4 5 6 13 joincl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
15 simprr 
 |-  ( ( K e. Poset /\ ( dom .\/ = ( B X. B ) /\ dom ./\ = ( B X. B ) ) ) -> dom ./\ = ( B X. B ) )
16 9 15 sylbi 
 |-  ( K e. Lat -> dom ./\ = ( B X. B ) )
17 16 3ad2ant1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> dom ./\ = ( B X. B ) )
18 8 17 eleqtrrd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> <. X , Y >. e. dom ./\ )
19 1 3 4 5 6 18 meetcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
20 14 19 jca 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X .\/ Y ) e. B /\ ( X ./\ Y ) e. B ) )