Metamath Proof Explorer

Theorem dicfnN

Description: Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dicfn.l ⊢ ≤ = ( le ‘ 𝐾 )
dicfn.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dicfn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dicfn.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
Assertion dicfnN ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } )

Proof

Step Hyp Ref Expression
1 dicfn.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dicfn.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 dicfn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dicfn.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
5 breq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ≤ 𝑊 ↔ 𝑞 ≤ 𝑊 ) )
6 5 notbid ⊢ ( 𝑝 = 𝑞 → ( ¬ 𝑝 ≤ 𝑊 ↔ ¬ 𝑞 ≤ 𝑊 ) )
7 6 elrab ⊢ ( 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↔ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) )
8 eqid ⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
11 1 2 3 8 9 10 4 dicval ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑞 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } )
12 fvex ⊢ ( 𝐼 ‘ 𝑞 ) ∈ V
13 11 12 eqeltrrdi ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ∈ V )
14 7 13 sylan2b ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ) → { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ∈ V )
15 14 ralrimiva ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ∈ V )
16 eqid ⊢ ( 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) = ( 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } )
17 16 fnmpt ⊢ ( ∀ 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ∈ V → ( 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) Fn { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } )
18 15 17 syl ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) Fn { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } )
19 1 2 3 8 9 10 4 dicfval ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) )
20 19 fneq1d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↔ ( 𝑞 ∈ { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑢 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑢 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) Fn { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } ) )
21 18 20 mpbird ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑝 ∈ 𝐴 ∣ ¬ 𝑝 ≤ 𝑊 } )