Metamath Proof Explorer

Theorem cvrval2

Description: Binary relation expressing Y covers X . Definition of covers in Kalmbach p. 15. ( cvbr2 analog.) (Contributed by NM, 16-Nov-2011)

Ref Expression
Hypotheses cvrletr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrletr.l ⊢ ≤ = ( le ‘ 𝐾 )
cvrletr.s ⊢ < = ( lt ‘ 𝐾 )
cvrletr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrval2 ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 cvrletr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrletr.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrletr.s ⊢ < = ( lt ‘ 𝐾 )
4 cvrletr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5 1 3 4 cvrval ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) ) )
6 iman ⊢ ( ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ↔ ¬ ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) ∧ ¬ 𝑧 = 𝑌 ) )
7 df-ne ⊢ ( 𝑧 ≠ 𝑌 ↔ ¬ 𝑧 = 𝑌 )
8 7 anbi2i ⊢ ( ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) ∧ 𝑧 ≠ 𝑌 ) ↔ ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) ∧ ¬ 𝑧 = 𝑌 ) )
9 6 8 xchbinxr ⊢ ( ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ↔ ¬ ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) ∧ 𝑧 ≠ 𝑌 ) )
10 anass ⊢ ( ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) ∧ 𝑧 ≠ 𝑌 ) ↔ ( 𝑋 < 𝑧 ∧ ( 𝑧 ≤ 𝑌 ∧ 𝑧 ≠ 𝑌 ) ) )
11 2 3 pltval ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑧 < 𝑌 ↔ ( 𝑧 ≤ 𝑌 ∧ 𝑧 ≠ 𝑌 ) ) )
12 11 3com23 ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 < 𝑌 ↔ ( 𝑧 ≤ 𝑌 ∧ 𝑧 ≠ 𝑌 ) ) )
13 12 3expa ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 < 𝑌 ↔ ( 𝑧 ≤ 𝑌 ∧ 𝑧 ≠ 𝑌 ) ) )
14 13 anbi2d ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ↔ ( 𝑋 < 𝑧 ∧ ( 𝑧 ≤ 𝑌 ∧ 𝑧 ≠ 𝑌 ) ) ) )
15 10 14 bitr4id ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) ∧ 𝑧 ≠ 𝑌 ) ↔ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) )
16 15 notbid ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ¬ ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) ∧ 𝑧 ≠ 𝑌 ) ↔ ¬ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) )
17 9 16 syl5bb ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ↔ ¬ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) )
18 17 ralbidva ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ↔ ∀ 𝑧 ∈ 𝐵 ¬ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) )
19 ralnex ⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ↔ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) )
20 18 19 bitrdi ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ↔ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) )
21 20 anbi2d ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 < 𝑌 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ) ↔ ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) ) )
22 21 3adant2 ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 < 𝑌 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ) ↔ ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) ) )
23 5 22 bitr4d ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 = 𝑌 ) ) ) )