Metamath Proof Explorer

Theorem cvbr

Description: Binary relation expressing B covers A , which means that B is larger than A and there is nothing in between. Definition 3.2.18 of PtakPulmannova p. 68. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvbr ⊢A∈Cℋ∧B∈Cℋ→A⋖ℋB↔A⊂B∧¬∃x∈CℋA⊂x∧x⊂B

Proof

Step Hyp Ref Expression
1 eleq1 ⊢y=A→y∈Cℋ↔A∈Cℋ
2 1 anbi1d ⊢y=A→y∈Cℋ∧z∈Cℋ↔A∈Cℋ∧z∈Cℋ
3 psseq1 ⊢y=A→y⊂z↔A⊂z
4 psseq1 ⊢y=A→y⊂x↔A⊂x
5 4 anbi1d ⊢y=A→y⊂x∧x⊂z↔A⊂x∧x⊂z
6 5 rexbidv ⊢y=A→∃x∈Cℋy⊂x∧x⊂z↔∃x∈CℋA⊂x∧x⊂z
7 6 notbid ⊢y=A→¬∃x∈Cℋy⊂x∧x⊂z↔¬∃x∈CℋA⊂x∧x⊂z
8 3 7 anbi12d ⊢y=A→y⊂z∧¬∃x∈Cℋy⊂x∧x⊂z↔A⊂z∧¬∃x∈CℋA⊂x∧x⊂z
9 2 8 anbi12d ⊢y=A→y∈Cℋ∧z∈Cℋ∧y⊂z∧¬∃x∈Cℋy⊂x∧x⊂z↔A∈Cℋ∧z∈Cℋ∧A⊂z∧¬∃x∈CℋA⊂x∧x⊂z
10 eleq1 ⊢z=B→z∈Cℋ↔B∈Cℋ
11 10 anbi2d ⊢z=B→A∈Cℋ∧z∈Cℋ↔A∈Cℋ∧B∈Cℋ
12 psseq2 ⊢z=B→A⊂z↔A⊂B
13 psseq2 ⊢z=B→x⊂z↔x⊂B
14 13 anbi2d ⊢z=B→A⊂x∧x⊂z↔A⊂x∧x⊂B
15 14 rexbidv ⊢z=B→∃x∈CℋA⊂x∧x⊂z↔∃x∈CℋA⊂x∧x⊂B
16 15 notbid ⊢z=B→¬∃x∈CℋA⊂x∧x⊂z↔¬∃x∈CℋA⊂x∧x⊂B
17 12 16 anbi12d ⊢z=B→A⊂z∧¬∃x∈CℋA⊂x∧x⊂z↔A⊂B∧¬∃x∈CℋA⊂x∧x⊂B
18 11 17 anbi12d ⊢z=B→A∈Cℋ∧z∈Cℋ∧A⊂z∧¬∃x∈CℋA⊂x∧x⊂z↔A∈Cℋ∧B∈Cℋ∧A⊂B∧¬∃x∈CℋA⊂x∧x⊂B
19 df-cv ⊢⋖ℋ=yz|y∈Cℋ∧z∈Cℋ∧y⊂z∧¬∃x∈Cℋy⊂x∧x⊂z
20 9 18 19 brabg ⊢A∈Cℋ∧B∈Cℋ→A⋖ℋB↔A∈Cℋ∧B∈Cℋ∧A⊂B∧¬∃x∈CℋA⊂x∧x⊂B
21 20 bianabs ⊢A∈Cℋ∧B∈Cℋ→A⋖ℋB↔A⊂B∧¬∃x∈CℋA⊂x∧x⊂B