Theorem cvcon3

Description: Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	cvcon3	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		chpsscon3	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
2		chpsscon3	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ⊊ 𝑥 ↔ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
3	2	adantlr	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ⊊ 𝑥 ↔ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
4		chpsscon3	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
5	4	ancoms	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
6	5	adantll	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
7	3 6	anbi12d	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ( ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) ) )
8		choccl	⊢ ( 𝑥 ∈ Cℋ → ( ⊥ ‘ 𝑥 ) ∈ Cℋ )
9		psseq2	⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ↔ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) )
10		psseq1	⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) )
11	9 10	anbi12d	⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
12	11	rspcev	⊢ ( ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) )
13	8 12	sylan	⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) )
14	13	ex	⊢ ( 𝑥 ∈ Cℋ → ( ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
15	14	ancomsd	⊢ ( 𝑥 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
16	15	adantl	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑥 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝑥 ) ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
17	7 16	sylbid	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
18	17	rexlimdva	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) → ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
19		chpsscon1	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ↔ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) )
20	19	adantll	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ↔ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) )
21		chpsscon2	⊢ ( ( 𝑦 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
22	21	ancoms	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
23	22	adantlr	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
24	20 23	anbi12d	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ∧ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) ) )
25		choccl	⊢ ( 𝑦 ∈ Cℋ → ( ⊥ ‘ 𝑦 ) ∈ Cℋ )
26		psseq2	⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝐴 ⊊ 𝑥 ↔ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) )
27		psseq1	⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 ⊊ 𝐵 ↔ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) )
28	26 27	anbi12d	⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) ) )
29	28	rspcev	⊢ ( ( ( ⊥ ‘ 𝑦 ) ∈ Cℋ ∧ ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) )
30	25 29	sylan	⊢ ( ( 𝑦 ∈ Cℋ ∧ ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) )
31	30	ex	⊢ ( 𝑦 ∈ Cℋ → ( ( 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
32	31	ancomsd	⊢ ( 𝑦 ∈ Cℋ → ( ( ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ∧ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
33	32	adantl	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝑦 ) ⊊ 𝐵 ∧ 𝐴 ⊊ ( ⊥ ‘ 𝑦 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
34	24 33	sylbid	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑦 ∈ Cℋ ) → ( ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
35	34	rexlimdva	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
36	18 35	impbid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
37	36	notbid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) )
38	1 37	anbi12d	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) ) )
39		cvbr	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) )
40		choccl	⊢ ( 𝐵 ∈ Cℋ → ( ⊥ ‘ 𝐵 ) ∈ Cℋ )
41		choccl	⊢ ( 𝐴 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )
42		cvbr	⊢ ( ( ( ⊥ ‘ 𝐵 ) ∈ Cℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) ) )
43	40 41 42	syl2anr	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ↔ ( ( ⊥ ‘ 𝐵 ) ⊊ ( ⊥ ‘ 𝐴 ) ∧ ¬ ∃ 𝑦 ∈ Cℋ ( ( ⊥ ‘ 𝐵 ) ⊊ 𝑦 ∧ 𝑦 ⊊ ( ⊥ ‘ 𝐴 ) ) ) ) )
44	38 39 43	3bitr4d	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⋖ℋ ( ⊥ ‘ 𝐴 ) ) )