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 syl5bi ⊢ ( 𝜑 → ( { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } → ∀ 𝑓 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
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 43 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑈 ∈ LVec )
45 5 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
47 1 2 8 9 11 45 46 dochsatshp ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ 𝑝 ) ∈ 𝐽 )
48 11 10 12 lshpkrex ⊢ ( ( 𝑈 ∈ LVec ∧ ( 𝑂 ‘ 𝑝 ) ∈ 𝐽 ) → ∃ 𝑓 ∈ 𝐹 ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) )
49 44 47 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝐹 ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) )
50 df-rex ⊢ ( ∃ 𝑓 ∈ 𝐹 ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ↔ ∃ 𝑓 ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) )
51 49 50 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) )
52 simprl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → 𝑓 ∈ 𝐹 )
53 simprr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) )
54 53 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) )
55 54 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) )
56 29 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑈 ∈ LMod )
57 19 9 56 46 lsatssv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ⊆ ( Base ‘ 𝑈 ) )
58 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
59 1 58 2 19 8 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ⊆ ( Base ‘ 𝑈 ) ) → ( 𝑂 ‘ 𝑝 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
60 45 57 59 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ 𝑝 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
61 1 58 8 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑂 ‘ 𝑝 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
62 45 60 61 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
64 55 63 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝑂 ‘ 𝑝 ) )
65 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ 𝑝 ) ∈ 𝐽 )
66 64 65 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ∈ 𝐽 )
67 52 66 31 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → 𝑓 ∈ 𝑇 )
68 1 2 58 9 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
69 45 46 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
70 1 58 8 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) = 𝑝 )
71 45 69 70 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) = 𝑝 )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑂 ‘ ( 𝑂 ‘ 𝑝 ) ) = 𝑝 )
73 54 72 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
74 67 73 jca ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) ) → ( 𝑓 ∈ 𝑇 ∧ 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
75 74 ex ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) → ( 𝑓 ∈ 𝑇 ∧ 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ) )
76 75 eximdv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑓 ( 𝑓 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝑓 ) = ( 𝑂 ‘ 𝑝 ) ) → ∃ 𝑓 ( 𝑓 ∈ 𝑇 ∧ 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) ) )
77 51 76 mpd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 ∈ 𝑇 ∧ 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
78 df-rex ⊢ ( ∃ 𝑓 ∈ 𝑇 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ∃ 𝑓 ( 𝑓 ∈ 𝑇 ∧ 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
79 77 78 sylibr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝑇 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
80 sseq1 ⊢ ( 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑝 ⊆ 𝑋 ↔ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ) )
81 sseq1 ⊢ ( 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) → ( 𝑝 ⊆ 𝑌 ↔ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) )
82 80 81 imbi12d ⊢ ( 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) → ( ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ 𝑌 ) ↔ ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) → ( ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ 𝑌 ) ↔ ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
84 42 79 83 ralxfrd ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ 𝑌 ) ↔ ∀ 𝑓 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ) )
85 30 84 bitr2d ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )
86 28 85 sylibd ⊢ ( 𝜑 → ( { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } → 𝑋 ⊆ 𝑌 ) )
87 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) ∧ 𝑓 ∈ 𝐶 ) → 𝑋 ⊆ 𝑌 )
88 sstr ⊢ ( ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑌 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 )
89 88 ancoms ⊢ ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 )
90 89 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) )
91 87 90 mpand ⊢ ( ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 ) )
92 91 ss2rabdv ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } )
93 92 ex ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } ) )
94 86 93 impbid ⊢ ( 𝜑 → ( { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑋 } ⊆ { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑌 } ↔ 𝑋 ⊆ 𝑌 ) )
95 17 94 bitrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )