Metamath Proof Explorer

Theorem dihcnvord

Description: Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses dihcnvord.l ⊢ ≤ ˙ = ≤ K
dihcnvord.h ⊢ H = LHyp ⁡ K
dihcnvord.i ⊢ I = DIsoH ⁡ K ⁡ W
dihcnvord.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihcnvord.x ⊢ φ → X ∈ ran ⁡ I
dihcnvord.y ⊢ φ → Y ∈ ran ⁡ I
Assertion dihcnvord ⊢ φ → I -1 ⁡ X ≤ ˙ I -1 ⁡ Y ↔ X ⊆ Y

Proof

Step Hyp Ref Expression
1 dihcnvord.l ⊢ ≤ ˙ = ≤ K
2 dihcnvord.h ⊢ H = LHyp ⁡ K
3 dihcnvord.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dihcnvord.k ⊢ φ → K ∈ HL ∧ W ∈ H
5 dihcnvord.x ⊢ φ → X ∈ ran ⁡ I
6 dihcnvord.y ⊢ φ → Y ∈ ran ⁡ I
7 eqid ⊢ Base K = Base K
8 7 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
9 4 5 8 syl2anc ⊢ φ → I -1 ⁡ X ∈ Base K
10 7 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I -1 ⁡ Y ∈ Base K
11 4 6 10 syl2anc ⊢ φ → I -1 ⁡ Y ∈ Base K
12 7 1 2 3 dihord ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ Y ∈ Base K → I ⁡ I -1 ⁡ X ⊆ I ⁡ I -1 ⁡ Y ↔ I -1 ⁡ X ≤ ˙ I -1 ⁡ Y
13 4 9 11 12 syl3anc ⊢ φ → I ⁡ I -1 ⁡ X ⊆ I ⁡ I -1 ⁡ Y ↔ I -1 ⁡ X ≤ ˙ I -1 ⁡ Y
14 2 3 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
15 4 5 14 syl2anc ⊢ φ → I ⁡ I -1 ⁡ X = X
16 2 3 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ Y = Y
17 4 6 16 syl2anc ⊢ φ → I ⁡ I -1 ⁡ Y = Y
18 15 17 sseq12d ⊢ φ → I ⁡ I -1 ⁡ X ⊆ I ⁡ I -1 ⁡ Y ↔ X ⊆ Y
19 13 18 bitr3d ⊢ φ → I -1 ⁡ X ≤ ˙ I -1 ⁡ Y ↔ X ⊆ Y