Theorem pmapfval

Description: The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011)

	Ref	Expression
Hypotheses	pmapfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapfval.l	⊢ ≤ = ( le ‘ 𝐾 )
	pmapfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pmapfval.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	pmapfval	⊢ ( 𝐾 ∈ 𝐶 → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		pmapfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pmapfval.l	⊢ ≤ = ( le ‘ 𝐾 )
3		pmapfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		pmapfval.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
5		elex	⊢ ( 𝐾 ∈ 𝐶 → 𝐾 ∈ V )
6		fveq2	⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
7	6 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
8		fveq2	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
9	8 3	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
10		fveq2	⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
11	10 2	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
12	11	breqd	⊢ ( 𝑘 = 𝐾 → ( 𝑎 ( le ‘ 𝑘 ) 𝑥 ↔ 𝑎 ≤ 𝑥 ) )
13	9 12	rabeqbidv	⊢ ( 𝑘 = 𝐾 → { 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑎 ( le ‘ 𝑘 ) 𝑥 } = { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } )
14	7 13	mpteq12dv	⊢ ( 𝑘 = 𝐾 → ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑎 ( le ‘ 𝑘 ) 𝑥 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )
15		df-pmap	⊢ pmap = ( 𝑘 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑎 ( le ‘ 𝑘 ) 𝑥 } ) )
16	14 15 1	mptfvmpt	⊢ ( 𝐾 ∈ V → ( pmap ‘ 𝐾 ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )
17	4 16	syl5eq	⊢ ( 𝐾 ∈ V → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )
18	5 17	syl	⊢ ( 𝐾 ∈ 𝐶 → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ { 𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥 } ) )