Theorem dihcnvord

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

	Ref	Expression
Hypotheses	dihcnvord.l	⊢ ≤ = ( le ‘ 𝐾 )
	dihcnvord.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihcnvord.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihcnvord.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dihcnvord.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
	dihcnvord.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
Assertion	dihcnvord	⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ≤ ( ◡ 𝐼 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		dihcnvord.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dihcnvord.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dihcnvord.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4		dihcnvord.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5		dihcnvord.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
6		dihcnvord.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8	7 2 3	dihcnvcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
9	4 5 8	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
10	7 2 3	dihcnvcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
11	4 6 10	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
12	7 1 2 3	dihord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ↔ ( ◡ 𝐼 ‘ 𝑋 ) ≤ ( ◡ 𝐼 ‘ 𝑌 ) ) )
13	4 9 11 12	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ↔ ( ◡ 𝐼 ‘ 𝑋 ) ≤ ( ◡ 𝐼 ‘ 𝑌 ) ) )
14	2 3	dihcnvid2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
15	4 5 14	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
16	2 3	dihcnvid2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
17	4 6 16	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
18	15 17	sseq12d	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ↔ 𝑋 ⊆ 𝑌 ) )
19	13 18	bitr3d	⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ≤ ( ◡ 𝐼 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )