Metamath Proof Explorer

Theorem mapd1o

Description: The map defined by df-mapd is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows M satisfies part of the definition of projectivity of Baer p. 40. TODO: change theorems leading to this ( lcfr , mapdrval , lclkrs , lclkr ,...) to use T i^i ~P C ? TODO: maybe get rid of $d's for g versus K U W ; propagate to mapdrn and any others. (Contributed by NM, 12-Mar-2015)

Ref Expression
Hypotheses mapd1o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapd1o.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapd1o.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapd1o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapd1o.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapd1o.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
mapd1o.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
mapd1o.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
mapd1o.t ⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
mapd1o.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
mapd1o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion mapd1o ( 𝜑 → 𝑀 : 𝑆 –1-1-onto→ ( 𝑇 ∩ 𝒫 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mapd1o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapd1o.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 mapd1o.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4 mapd1o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 mapd1o.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6 mapd1o.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 mapd1o.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 mapd1o.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
9 mapd1o.t ⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
10 mapd1o.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
11 mapd1o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 6 fvexi ⊢ 𝐹 ∈ V
13 12 rabex ⊢ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑡 ) } ∈ V
14 eqid ⊢ ( 𝑡 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑡 ) } ) = ( 𝑡 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑡 ) } )
15 13 14 fnmpti ⊢ ( 𝑡 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑡 ) } ) Fn 𝑆
16 1 4 5 6 7 2 3 mapdfval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑡 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑡 ) } ) )
17 11 16 syl ⊢ ( 𝜑 → 𝑀 = ( 𝑡 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑡 ) } ) )
18 17 fneq1d ⊢ ( 𝜑 → ( 𝑀 Fn 𝑆 ↔ ( 𝑡 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑡 ) } ) Fn 𝑆 ) )
19 15 18 mpbiri ⊢ ( 𝜑 → 𝑀 Fn 𝑆 )
20 12 rabex ⊢ { 𝑔 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑡 ) } ∈ V
21 eqid ⊢ ( 𝑡 ∈ 𝑆 ↦ { 𝑔 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑡 ) } ) = ( 𝑡 ∈ 𝑆 ↦ { 𝑔 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑡 ) } )
22 20 21 fnmpti ⊢ ( 𝑡 ∈ 𝑆 ↦ { 𝑔 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑡 ) } ) Fn 𝑆
23 1 4 5 6 7 2 3 mapdfval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑡 ∈ 𝑆 ↦ { 𝑔 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑡 ) } ) )
24 11 23 syl ⊢ ( 𝜑 → 𝑀 = ( 𝑡 ∈ 𝑆 ↦ { 𝑔 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑡 ) } ) )
25 24 fneq1d ⊢ ( 𝜑 → ( 𝑀 Fn 𝑆 ↔ ( 𝑡 ∈ 𝑆 ↦ { 𝑔 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑡 ) } ) Fn 𝑆 ) )
26 22 25 mpbiri ⊢ ( 𝜑 → 𝑀 Fn 𝑆 )
27 fvelrnb ⊢ ( 𝑀 Fn 𝑆 → ( 𝑡 ∈ ran 𝑀 ↔ ∃ 𝑐 ∈ 𝑆 ( 𝑀 ‘ 𝑐 ) = 𝑡 ) )
28 26 27 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ran 𝑀 ↔ ∃ 𝑐 ∈ 𝑆 ( 𝑀 ‘ 𝑐 ) = 𝑡 ) )
29 11 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑆 ) → 𝑐 ∈ 𝑆 )
31 1 4 5 6 7 2 3 29 30 mapdval ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑐 ) = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } )
32 eqid ⊢ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) }
33 1 2 4 5 6 7 8 9 10 32 29 30 lclkrs2 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑆 ) → ( { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝑇 ∧ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ⊆ 𝐶 ) )
34 elin ⊢ ( { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ↔ ( { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝑇 ∧ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝒫 𝐶 ) )
35 12 rabex ⊢ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ V
36 35 elpw ⊢ ( { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝒫 𝐶 ↔ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ⊆ 𝐶 )
37 36 anbi2i ⊢ ( ( { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝑇 ∧ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝒫 𝐶 ) ↔ ( { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝑇 ∧ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ⊆ 𝐶 ) )
38 34 37 bitr2i ⊢ ( ( { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ 𝑇 ∧ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ⊆ 𝐶 ) ↔ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ ( 𝑇 ∩ 𝒫 𝐶 ) )
39 33 38 sylib ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑆 ) → { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑐 ) } ∈ ( 𝑇 ∩ 𝒫 𝐶 ) )
40 31 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑐 ) ∈ ( 𝑇 ∩ 𝒫 𝐶 ) )
41 eleq1 ⊢ ( ( 𝑀 ‘ 𝑐 ) = 𝑡 → ( ( 𝑀 ‘ 𝑐 ) ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ↔ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) )
42 40 41 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑆 ) → ( ( 𝑀 ‘ 𝑐 ) = 𝑡 → 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) )
43 42 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝑆 ( 𝑀 ‘ 𝑐 ) = 𝑡 → 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) )
44 eqid ⊢ ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) )
45 11 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
46 inss1 ⊢ ( 𝑇 ∩ 𝒫 𝐶 ) ⊆ 𝑇
47 46 sseli ⊢ ( 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) → 𝑡 ∈ 𝑇 )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) → 𝑡 ∈ 𝑇 )
49 inss2 ⊢ ( 𝑇 ∩ 𝒫 𝐶 ) ⊆ 𝒫 𝐶
50 49 sseli ⊢ ( 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) → 𝑡 ∈ 𝒫 𝐶 )
51 50 elpwid ⊢ ( 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) → 𝑡 ⊆ 𝐶 )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) → 𝑡 ⊆ 𝐶 )
53 1 2 4 5 6 7 8 9 10 44 45 48 52 lcfr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) → ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝑆 )
54 1 2 3 4 5 6 7 8 9 10 45 48 52 44 mapdrval ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) → ( 𝑀 ‘ ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = 𝑡 )
55 fveqeq2 ⊢ ( 𝑐 = ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) → ( ( 𝑀 ‘ 𝑐 ) = 𝑡 ↔ ( 𝑀 ‘ ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = 𝑡 ) )
56 55 rspcev ⊢ ( ( ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝑆 ∧ ( 𝑀 ‘ ∪ 𝑓 ∈ 𝑡 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = 𝑡 ) → ∃ 𝑐 ∈ 𝑆 ( 𝑀 ‘ 𝑐 ) = 𝑡 )
57 53 54 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) → ∃ 𝑐 ∈ 𝑆 ( 𝑀 ‘ 𝑐 ) = 𝑡 )
58 57 ex ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) → ∃ 𝑐 ∈ 𝑆 ( 𝑀 ‘ 𝑐 ) = 𝑡 ) )
59 43 58 impbid ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝑆 ( 𝑀 ‘ 𝑐 ) = 𝑡 ↔ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) )
60 28 59 bitrd ⊢ ( 𝜑 → ( 𝑡 ∈ ran 𝑀 ↔ 𝑡 ∈ ( 𝑇 ∩ 𝒫 𝐶 ) ) )
61 60 eqrdv ⊢ ( 𝜑 → ran 𝑀 = ( 𝑇 ∩ 𝒫 𝐶 ) )
62 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
63 simprl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑡 ∈ 𝑆 )
64 simprr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → 𝑢 ∈ 𝑆 )
65 1 4 5 3 62 63 64 mapd11 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑀 ‘ 𝑡 ) = ( 𝑀 ‘ 𝑢 ) ↔ 𝑡 = 𝑢 ) )
66 65 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( 𝑀 ‘ 𝑡 ) = ( 𝑀 ‘ 𝑢 ) → 𝑡 = 𝑢 ) )
67 66 ralrimivva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑀 ‘ 𝑡 ) = ( 𝑀 ‘ 𝑢 ) → 𝑡 = 𝑢 ) )
68 dff1o6 ⊢ ( 𝑀 : 𝑆 –1-1-onto→ ( 𝑇 ∩ 𝒫 𝐶 ) ↔ ( 𝑀 Fn 𝑆 ∧ ran 𝑀 = ( 𝑇 ∩ 𝒫 𝐶 ) ∧ ∀ 𝑡 ∈ 𝑆 ∀ 𝑢 ∈ 𝑆 ( ( 𝑀 ‘ 𝑡 ) = ( 𝑀 ‘ 𝑢 ) → 𝑡 = 𝑢 ) ) )
69 19 61 67 68 syl3anbrc ⊢ ( 𝜑 → 𝑀 : 𝑆 –1-1-onto→ ( 𝑇 ∩ 𝒫 𝐶 ) )