# Metamath Proof Explorer

## Theorem cvrval4N

Description: Binary relation expressing Y covers X . (Contributed by NM, 16-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cvrval4.b 𝐵 = ( Base ‘ 𝐾 )
cvrval4.s < = ( lt ‘ 𝐾 )
cvrval4.j = ( join ‘ 𝐾 )
cvrval4.c 𝐶 = ( ⋖ ‘ 𝐾 )
cvrval4.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrval4N ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 ) ) )

### Proof

Step Hyp Ref Expression
1 cvrval4.b 𝐵 = ( Base ‘ 𝐾 )
2 cvrval4.s < = ( lt ‘ 𝐾 )
3 cvrval4.j = ( join ‘ 𝐾 )
4 cvrval4.c 𝐶 = ( ⋖ ‘ 𝐾 )
5 cvrval4.a 𝐴 = ( Atoms ‘ 𝐾 )
6 1 2 4 cvrlt ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
7 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 1 7 3 4 5 cvrval3 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ∃ 𝑝𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 𝑝 ) = 𝑌 ) ) )
9 simpr ( ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ( 𝑋 𝑝 ) = 𝑌 )
10 9 reximi ( ∃ 𝑝𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 )
11 8 10 syl6bi ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 → ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 ) )
12 11 imp ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 )
13 6 12 jca ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 < 𝑌 ∧ ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 ) )
14 13 ex ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 → ( 𝑋 < 𝑌 ∧ ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 ) ) )
15 simp1r ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → 𝑋 < 𝑌 )
16 simp3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ( 𝑋 𝑝 ) = 𝑌 )
17 15 16 breqtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → 𝑋 < ( 𝑋 𝑝 ) )
18 simp1l1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → 𝐾 ∈ HL )
19 simp1l2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → 𝑋𝐵 )
20 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → 𝑝𝐴 )
21 1 7 3 4 5 cvr1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑝𝐴 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋𝑋 𝐶 ( 𝑋 𝑝 ) ) )
22 18 19 20 21 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋𝑋 𝐶 ( 𝑋 𝑝 ) ) )
23 1 2 3 4 5 cvr2N ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑝𝐴 ) → ( 𝑋 < ( 𝑋 𝑝 ) ↔ 𝑋 𝐶 ( 𝑋 𝑝 ) ) )
24 18 19 20 23 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ( 𝑋 < ( 𝑋 𝑝 ) ↔ 𝑋 𝐶 ( 𝑋 𝑝 ) ) )
25 22 24 bitr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋𝑋 < ( 𝑋 𝑝 ) ) )
26 17 25 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 )
27 26 16 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝𝐴 ∧ ( 𝑋 𝑝 ) = 𝑌 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 𝑝 ) = 𝑌 ) )
28 27 3exp ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑝𝐴 → ( ( 𝑋 𝑝 ) = 𝑌 → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 𝑝 ) = 𝑌 ) ) ) )
29 28 reximdvai ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 → ∃ 𝑝𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 𝑝 ) = 𝑌 ) ) )
30 29 expimpd ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 < 𝑌 ∧ ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 ) → ∃ 𝑝𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 𝑝 ) = 𝑌 ) ) )
31 30 8 sylibrd ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 < 𝑌 ∧ ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 ) → 𝑋 𝐶 𝑌 ) )
32 14 31 impbid ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ∃ 𝑝𝐴 ( 𝑋 𝑝 ) = 𝑌 ) ) )