Theorem diaord

Description: The partial isomorphism A for a lattice K is order-preserving in the region under co-atom W . Part of Lemma M of Crawley p. 120 line 28. (Contributed by NM, 26-Nov-2013)

	Ref	Expression
Hypotheses	dia11.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dia11.l	⊢ ≤ = ( le ‘ 𝐾 )
	dia11.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dia11.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion	diaord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		dia11.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dia11.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dia11.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dia11.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7	1 2 3 5 6 4	diaval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } )
8	7	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } )
9	1 2 3 5 6 4	diaval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑌 ) = { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑌 } )
10	9	3adant2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑌 ) = { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑌 } )
11	8 10	sseq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } ⊆ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑌 } ) )
12		ss2rab	⊢ ( { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } ⊆ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑌 } ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑌 ) )
13		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
14	1 2 13 3 5 6	trlord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑌 ) ) )
15	12 14	bitr4id	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } ⊆ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑌 } ↔ 𝑋 ≤ 𝑌 ) )
16	11 15	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) )