# Metamath Proof Explorer

## Theorem cvrval5

Description: Binary relation expressing X covers X ./\ Y . (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses cvrval5.b 𝐵 = ( Base ‘ 𝐾 )
cvrval5.l = ( le ‘ 𝐾 )
cvrval5.j = ( join ‘ 𝐾 )
cvrval5.m = ( meet ‘ 𝐾 )
cvrval5.c 𝐶 = ( ⋖ ‘ 𝐾 )
cvrval5.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrval5 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝𝐴 ( ¬ 𝑝 𝑌 ∧ ( 𝑝 ( 𝑋 𝑌 ) ) = 𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 cvrval5.b 𝐵 = ( Base ‘ 𝐾 )
2 cvrval5.l = ( le ‘ 𝐾 )
3 cvrval5.j = ( join ‘ 𝐾 )
4 cvrval5.m = ( meet ‘ 𝐾 )
5 cvrval5.c 𝐶 = ( ⋖ ‘ 𝐾 )
6 cvrval5.a 𝐴 = ( Atoms ‘ 𝐾 )
7 simp1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → 𝐾 ∈ HL )
8 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
10 8 9 syl3an1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
11 simp2 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → 𝑋𝐵 )
12 1 2 3 5 6 cvrval3 ( ( 𝐾 ∈ HL ∧ ( 𝑋 𝑌 ) ∈ 𝐵𝑋𝐵 ) → ( ( 𝑋 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝𝐴 ( ¬ 𝑝 ( 𝑋 𝑌 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) ) )
13 7 10 11 12 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝𝐴 ( ¬ 𝑝 ( 𝑋 𝑌 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) ) )
14 8 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → 𝐾 ∈ Lat )
15 14 ad2antrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → 𝐾 ∈ Lat )
16 10 ad2antrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
17 1 6 atbase ( 𝑝𝐴𝑝𝐵 )
18 17 ad2antlr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → 𝑝𝐵 )
19 1 2 3 latlej2 ( ( 𝐾 ∈ Lat ∧ ( 𝑋 𝑌 ) ∈ 𝐵𝑝𝐵 ) → 𝑝 ( ( 𝑋 𝑌 ) 𝑝 ) )
20 15 16 18 19 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → 𝑝 ( ( 𝑋 𝑌 ) 𝑝 ) )
21 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 )
22 20 21 breqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → 𝑝 𝑋 )
23 22 biantrurd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → ( 𝑝 𝑌 ↔ ( 𝑝 𝑋𝑝 𝑌 ) ) )
24 simpll2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → 𝑋𝐵 )
25 simpll3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → 𝑌𝐵 )
26 1 2 4 latlem12 ( ( 𝐾 ∈ Lat ∧ ( 𝑝𝐵𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑝 𝑋𝑝 𝑌 ) ↔ 𝑝 ( 𝑋 𝑌 ) ) )
27 15 18 24 25 26 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → ( ( 𝑝 𝑋𝑝 𝑌 ) ↔ 𝑝 ( 𝑋 𝑌 ) ) )
28 23 27 bitr2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → ( 𝑝 ( 𝑋 𝑌 ) ↔ 𝑝 𝑌 ) )
29 28 notbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) → ( ¬ 𝑝 ( 𝑋 𝑌 ) ↔ ¬ 𝑝 𝑌 ) )
30 29 ex ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → ( ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 → ( ¬ 𝑝 ( 𝑋 𝑌 ) ↔ ¬ 𝑝 𝑌 ) ) )
31 30 pm5.32rd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → ( ( ¬ 𝑝 ( 𝑋 𝑌 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 𝑌 ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) ) )
32 14 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → 𝐾 ∈ Lat )
33 10 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
34 17 adantl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → 𝑝𝐵 )
35 1 3 latjcom ( ( 𝐾 ∈ Lat ∧ ( 𝑋 𝑌 ) ∈ 𝐵𝑝𝐵 ) → ( ( 𝑋 𝑌 ) 𝑝 ) = ( 𝑝 ( 𝑋 𝑌 ) ) )
36 32 33 34 35 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → ( ( 𝑋 𝑌 ) 𝑝 ) = ( 𝑝 ( 𝑋 𝑌 ) ) )
37 36 eqeq1d ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → ( ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ↔ ( 𝑝 ( 𝑋 𝑌 ) ) = 𝑋 ) )
38 37 anbi2d ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → ( ( ¬ 𝑝 𝑌 ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 𝑌 ∧ ( 𝑝 ( 𝑋 𝑌 ) ) = 𝑋 ) ) )
39 31 38 bitrd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑝𝐴 ) → ( ( ¬ 𝑝 ( 𝑋 𝑌 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 𝑌 ∧ ( 𝑝 ( 𝑋 𝑌 ) ) = 𝑋 ) ) )
40 39 rexbidva ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( ∃ 𝑝𝐴 ( ¬ 𝑝 ( 𝑋 𝑌 ) ∧ ( ( 𝑋 𝑌 ) 𝑝 ) = 𝑋 ) ↔ ∃ 𝑝𝐴 ( ¬ 𝑝 𝑌 ∧ ( 𝑝 ( 𝑋 𝑌 ) ) = 𝑋 ) ) )
41 13 40 bitrd ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 𝑌 ) 𝐶 𝑋 ↔ ∃ 𝑝𝐴 ( ¬ 𝑝 𝑌 ∧ ( 𝑝 ( 𝑋 𝑌 ) ) = 𝑋 ) ) )