Definition df-disoa 40972

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

Assertion

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

Distinct variable group:   𝑤,𝑘,𝑥,𝑦,𝑓

Detailed syntax breakdown of Definition df-disoa

Step	Hyp	Ref	Expression
1		cdia 40971	. 2 class DIsoA
2		vk	. . 3 setvar 𝑘
3		cvv 3464	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 39927	. . . . 5 class LHyp
7	5, 6	cfv 6542	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1538	. . . . . . 7 class 𝑦
11	4	cv 1538	. . . . . . 7 class 𝑤
12		cple 17284	. . . . . . . 8 class le
13	5, 12	cfv 6542	. . . . . . 7 class (le‘𝑘)
14	10, 11, 13	wbr 5125	. . . . . 6 wff 𝑦(le‘𝑘)𝑤
15		cbs 17230	. . . . . . 7 class Base
16	5, 15	cfv 6542	. . . . . 6 class (Base‘𝑘)
17	14, 9, 16	crab 3420	. . . . 5 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤}
18		vf	. . . . . . . . 9 setvar 𝑓
19	18	cv 1538	. . . . . . . 8 class 𝑓
20		ctrl 40101	. . . . . . . . . 10 class trL
21	5, 20	cfv 6542	. . . . . . . . 9 class (trL‘𝑘)
22	11, 21	cfv 6542	. . . . . . . 8 class ((trL‘𝑘)‘𝑤)
23	19, 22	cfv 6542	. . . . . . 7 class (((trL‘𝑘)‘𝑤)‘𝑓)
24	8	cv 1538	. . . . . . 7 class 𝑥
25	23, 24, 13	wbr 5125	. . . . . 6 wff (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥
26		cltrn 40044	. . . . . . . 8 class LTrn
27	5, 26	cfv 6542	. . . . . . 7 class (LTrn‘𝑘)
28	11, 27	cfv 6542	. . . . . 6 class ((LTrn‘𝑘)‘𝑤)
29	25, 18, 28	crab 3420	. . . . 5 class {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}
30	8, 17, 29	cmpt 5207	. . . 4 class (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})
31	4, 7, 30	cmpt 5207	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}))
32	2, 3, 31	cmpt 5207	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
33	1, 32	wceq 1539	1 wff DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))

This definition is referenced by:  diaffval  40973