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 ‘ 𝑘 ) 𝑥 } ) ) )