Metamath Proof Explorer

Theorem mapdordlem2

Description: Lemma for mapdord . Ordering property of projectivity M . TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the T hypothesis. (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses mapdord.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdord.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdord.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapdord.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdord.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdord.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
mapdord.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
mapdord.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdord.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
mapdord.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
mapdord.c ⊢ 𝐽 = ( LSHyp ‘ 𝑈 )
mapdord.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
mapdord.t ⊢ 𝑇 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝐽 }
mapdord.q ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
Assertion mapdordlem2 ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mapdord.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdord.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdord.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
4 mapdord.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
5 mapdord.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 mapdord.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
7 mapdord.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
8 mapdord.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
9 mapdord.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
10 mapdord.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
11 mapdord.c ⊢ 𝐽 = ( LSHyp ‘ 𝑈 )
12 mapdord.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
13 mapdord.t ⊢ 𝑇 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∈ 𝐽 }
14 mapdord.q ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
15 1 2 3 10 12 8 4 5 6 14 mapdvalc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) = { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } )
16 1 2 3 10 12 8 4 5 7 14 mapdvalc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) = { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } )
17 15 16 sseq12d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ↔ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } ) )
18 ss2rab ⊢ ( { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } ↔ ∀ 𝑓 ∈ 𝐶 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) )
19 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20 1 8 2 19 11 10 12 13 14 5 mapdordlem1a ⊢ ( 𝜑 → ( 𝑓 ∈ 𝑇 ↔ ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 ) ) )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 ) ) → 𝑓 ∈ 𝐶 )
22 idd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 ) ) → ( ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
23 21 22 embantd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 ) ) → ( ( 𝑓 ∈ 𝐶 → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
24 23 ex ⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 ) → ( ( 𝑓 ∈ 𝐶 → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) ) )
25 20 24 sylbid ⊢ ( 𝜑 → ( 𝑓 ∈ 𝑇 → ( ( 𝑓 ∈ 𝐶 → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) ) )
26 25 com23 ⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝐶 → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) → ( 𝑓 ∈ 𝑇 → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) ) )
27 26 ralimdv2 ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ 𝐶 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) → ∀ 𝑓 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
28 18 27 biimtrid ⊢ ( 𝜑 → ( { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } → ∀ 𝑓 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
29 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
30 3 9 29 6 7 lssatle ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ 𝑌 ) ) )
31 13 mapdordlem1 ⊢ ( 𝑓 ∈ 𝑇 ↔ ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 ) )
32 31 simprbi ⊢ ( 𝑓 ∈ 𝑇 → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 )
34 5 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35 31 simplbi ⊢ ( 𝑓 ∈ 𝑇 → 𝑓 ∈ 𝐹 )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ 𝐹 )
37 1 8 2 10 11 12 34 36 dochlkr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝐿 ‘ 𝑓 ) ∈ 𝐽 ) ) )
38 33 37 mpbid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝐿 ‘ 𝑓 ) ∈ 𝐽 ) )
39 38 simpld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) )
40 38 simprd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝐿 ‘ 𝑓 ) ∈ 𝐽 )
41 1 8 2 9 11 34 40 dochshpsat ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ↔ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝐴 ) )
42 39 41 mpbid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝐴 )
43 1 2 5 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
44 5 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
45 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
46 1 2 8 9 11 44 45 dochsatshp ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ 𝑝 ) ∈ 𝐽 )
47 11 10 12 lshpkrex ⊢ ( ( 𝑈 ∈ LVec ∧ ( 𝑂 ‘ 𝑝 ) ∈ 𝐽 ) → ∃ 𝑓 ∈ 𝐹 ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) )
48 43 46 47 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝐹 ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) )
49 simprl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → 𝑓 ∈ 𝐹 )
50 simprr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) )
51 50 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) )
52 51 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) )
53 29 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑈 ∈ LMod )
54 19 9 53 45 lsatssv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ⊆ ( Base ‘ 𝑈 ) )
55 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
56 1 55 2 19 8 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑂 ‘ 𝑝 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
57 5 54 56 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ 𝑝 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
58 1 55 8 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑂 ‘ 𝑝 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
59 5 57 58 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
60 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
61 52 60 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
62 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ 𝑝 ) ∈ 𝐽 )
63 61 62 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 )
64 49 63 31 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → 𝑓 ∈ 𝑇 )
65 1 2 55 9 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
66 5 45 65 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
67 1 55 8 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) = 𝑝 )
68 5 66 67 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) = 𝑝 )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) = 𝑝 )
70 51 69 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
71 48 64 70 reximssdv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝑇 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
72 sseq1 ⊢ ( 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑝 ⊆ 𝑋 ↔ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ) )
73 sseq1 ⊢ ( 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑝 ⊆ 𝑌 ↔ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) )
74 72 73 imbi12d ⊢ ( 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) → ( ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ 𝑌 ) ↔ ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) → ( ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ 𝑌 ) ↔ ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
76 42 71 75 ralxfrd ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ 𝑌 ) ↔ ∀ 𝑓 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
77 30 76 bitr2d ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )
78 28 77 sylibd ⊢ ( 𝜑 → ( { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } → 𝑋 ⊆ 𝑌 ) )
79 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) ∧ 𝑓 ∈ 𝐶 ) → 𝑋 ⊆ 𝑌 )
80 sstr ⊢ ( ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑌 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 )
81 80 ancoms ⊢ ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 )
82 81 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) )
83 79 82 mpand ⊢ ( ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) )
84 83 ss2rabdv ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } )
85 84 ex ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } ) )
86 78 85 impbid ⊢ ( 𝜑 → ( { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } ↔ 𝑋 ⊆ 𝑌 ) )
87 17 86 bitrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )