This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islat

Description: The predicate "is a lattice". (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)

Ref Expression
Hypotheses islat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
islat.j ⊢ ∨ = ( join ‘ 𝐾 )
islat.m ⊢ ∧ = ( meet ‘ 𝐾 )
Assertion islat ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 islat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 islat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 islat.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 fveq2 ⊢ ( 𝑙 = 𝐾 → ( join ‘ 𝑙 ) = ( join ‘ 𝐾 ) )
5 4 2 eqtr4di ⊢ ( 𝑙 = 𝐾 → ( join ‘ 𝑙 ) = ∨ )
6 5 dmeqd ⊢ ( 𝑙 = 𝐾 → dom ( join ‘ 𝑙 ) = dom ∨ )
7 fveq2 ⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = ( Base ‘ 𝐾 ) )
8 7 1 eqtr4di ⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = 𝐵 )
9 8 sqxpeqd ⊢ ( 𝑙 = 𝐾 → ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) = ( 𝐵 × 𝐵 ) )
10 6 9 eqeq12d ⊢ ( 𝑙 = 𝐾 → ( dom ( join ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ↔ dom ∨ = ( 𝐵 × 𝐵 ) ) )
11 fveq2 ⊢ ( 𝑙 = 𝐾 → ( meet ‘ 𝑙 ) = ( meet ‘ 𝐾 ) )
12 11 3 eqtr4di ⊢ ( 𝑙 = 𝐾 → ( meet ‘ 𝑙 ) = ∧ )
13 12 dmeqd ⊢ ( 𝑙 = 𝐾 → dom ( meet ‘ 𝑙 ) = dom ∧ )
14 13 9 eqeq12d ⊢ ( 𝑙 = 𝐾 → ( dom ( meet ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ↔ dom ∧ = ( 𝐵 × 𝐵 ) ) )
15 10 14 anbi12d ⊢ ( 𝑙 = 𝐾 → ( ( dom ( join ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ∧ dom ( meet ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ) ↔ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )
16 df-lat ⊢ Lat = { 𝑙 ∈ Poset ∣ ( dom ( join ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ∧ dom ( meet ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ) }
17 15 16 elrab2 ⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )