Metamath Proof Explorer


Theorem cvrcon3b

Description: Contraposition law for the covers relation. ( cvcon3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses cvrcon3b.b 𝐵 = ( Base ‘ 𝐾 )
cvrcon3b.o = ( oc ‘ 𝐾 )
cvrcon3b.c 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrcon3b ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑌 ) 𝐶 ( 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 cvrcon3b.b 𝐵 = ( Base ‘ 𝐾 )
2 cvrcon3b.o = ( oc ‘ 𝐾 )
3 cvrcon3b.c 𝐶 = ( ⋖ ‘ 𝐾 )
4 eqid ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
5 1 4 2 opltcon3b ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) )
6 simpl1 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → 𝐾 ∈ OP )
7 simpl2 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → 𝑋𝐵 )
8 simpr ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → 𝑥𝐵 )
9 1 4 2 opltcon3b ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑥𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ↔ ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) )
10 6 7 8 9 syl3anc ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ↔ ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) )
11 simpl3 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → 𝑌𝐵 )
12 1 4 2 opltcon3b ( ( 𝐾 ∈ OP ∧ 𝑥𝐵𝑌𝐵 ) → ( 𝑥 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ) )
13 6 8 11 12 syl3anc ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑥 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ) )
14 10 13 anbi12d ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ∧ ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ) ) )
15 1 2 opoccl ( ( 𝐾 ∈ OP ∧ 𝑥𝐵 ) → ( 𝑥 ) ∈ 𝐵 )
16 15 3ad2antl1 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑥 ) ∈ 𝐵 )
17 breq2 ( 𝑦 = ( 𝑥 ) → ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ↔ ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ) )
18 breq1 ( 𝑦 = ( 𝑥 ) → ( 𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ↔ ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) )
19 17 18 anbi12d ( 𝑦 = ( 𝑥 ) → ( ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ↔ ( ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ∧ ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
20 19 rspcev ( ( ( 𝑥 ) ∈ 𝐵 ∧ ( ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ∧ ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) → ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) )
21 20 ex ( ( 𝑥 ) ∈ 𝐵 → ( ( ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ∧ ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) → ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
22 16 21 syl ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → ( ( ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ∧ ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ) → ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
23 22 ancomsd ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → ( ( ( 𝑥 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ∧ ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑥 ) ) → ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
24 14 23 sylbid ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑥𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
25 24 rexlimdva ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
26 simpl1 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → 𝐾 ∈ OP )
27 simpl3 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → 𝑌𝐵 )
28 simpr ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → 𝑦𝐵 )
29 1 4 2 opltcon1b ( ( 𝐾 ∈ OP ∧ 𝑌𝐵𝑦𝐵 ) → ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ↔ ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) )
30 26 27 28 29 syl3anc ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ↔ ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) )
31 simpl2 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → 𝑋𝐵 )
32 1 4 2 opltcon2b ( ( 𝐾 ∈ OP ∧ 𝑦𝐵𝑋𝐵 ) → ( 𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ↔ 𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ) )
33 26 28 31 32 syl3anc ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → ( 𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ↔ 𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ) )
34 30 33 anbi12d ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → ( ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ↔ ( ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ) ) )
35 1 2 opoccl ( ( 𝐾 ∈ OP ∧ 𝑦𝐵 ) → ( 𝑦 ) ∈ 𝐵 )
36 35 3ad2antl1 ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → ( 𝑦 ) ∈ 𝐵 )
37 breq2 ( 𝑥 = ( 𝑦 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ) )
38 breq1 ( 𝑥 = ( 𝑦 ) → ( 𝑥 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) )
39 37 38 anbi12d ( 𝑥 = ( 𝑦 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ∧ ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) ) )
40 39 rspcev ( ( ( 𝑦 ) ∈ 𝐵 ∧ ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ∧ ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) )
41 40 ex ( ( 𝑦 ) ∈ 𝐵 → ( ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ∧ ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) )
42 36 41 syl ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ∧ ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) )
43 42 ancomsd ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → ( ( ( 𝑦 ) ( lt ‘ 𝐾 ) 𝑌𝑋 ( lt ‘ 𝐾 ) ( 𝑦 ) ) → ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) )
44 34 43 sylbid ( ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑦𝐵 ) → ( ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) → ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) )
45 44 rexlimdva ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) → ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) )
46 25 45 impbid ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
47 46 notbid ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( ¬ ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ¬ ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) )
48 5 47 anbi12d ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ↔ ( ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ∧ ¬ ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) ) )
49 1 4 3 cvrval ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑥𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ) )
50 simp1 ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → 𝐾 ∈ OP )
51 1 2 opoccl ( ( 𝐾 ∈ OP ∧ 𝑌𝐵 ) → ( 𝑌 ) ∈ 𝐵 )
52 51 3adant2 ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑌 ) ∈ 𝐵 )
53 1 2 opoccl ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → ( 𝑋 ) ∈ 𝐵 )
54 53 3adant3 ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 ) ∈ 𝐵 )
55 1 4 3 cvrval ( ( 𝐾 ∈ OP ∧ ( 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ) ∈ 𝐵 ) → ( ( 𝑌 ) 𝐶 ( 𝑋 ) ↔ ( ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ∧ ¬ ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) ) )
56 50 52 54 55 syl3anc ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑌 ) 𝐶 ( 𝑋 ) ↔ ( ( 𝑌 ) ( lt ‘ 𝐾 ) ( 𝑋 ) ∧ ¬ ∃ 𝑦𝐵 ( ( 𝑌 ) ( lt ‘ 𝐾 ) 𝑦𝑦 ( lt ‘ 𝐾 ) ( 𝑋 ) ) ) ) )
57 48 49 56 3bitr4d ( ( 𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑌 ) 𝐶 ( 𝑋 ) ) )