This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-disoa

Description: Define partial isomorphism A. (Contributed by NM, 15-Oct-2013)

Ref Expression
Assertion df-disoa DIsoA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdia ⊢ DIsoA
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 vx ⊢ 𝑥
8 vy ⊢ 𝑦
9 cbs ⊢ Base
10 5 9 cfv ⊢ ( Base ‘ 𝑘 )
11 8 cv ⊢ 𝑦
12 cple ⊢ le
13 5 12 cfv ⊢ ( le ‘ 𝑘 )
14 3 cv ⊢ 𝑤
15 11 14 13 wbr ⊢ 𝑦 ( le ‘ 𝑘 ) 𝑤
16 15 8 10 crab ⊢ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 }
17 vf ⊢ 𝑓
18 cltrn ⊢ LTrn
19 5 18 cfv ⊢ ( LTrn ‘ 𝑘 )
20 14 19 cfv ⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
21 ctrl ⊢ trL
22 5 21 cfv ⊢ ( trL ‘ 𝑘 )
23 14 22 cfv ⊢ ( ( trL ‘ 𝑘 ) ‘ 𝑤 )
24 17 cv ⊢ 𝑓
25 24 23 cfv ⊢ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 )
26 7 cv ⊢ 𝑥
27 25 26 13 wbr ⊢ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥
28 27 17 20 crab ⊢ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 }
29 7 16 28 cmpt ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } )
30 3 6 29 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } ) )
31 1 2 30 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } ) ) )
32 0 31 wceq ⊢ DIsoA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } ) ) )