Metamath Proof Explorer

Definition df-dilN

Description: Define set of all dilations. Definition of dilation in Crawley p. 111. (Contributed by NM, 30-Jan-2012)

Ref Expression
Assertion df-dilN ⊢Dil=k∈V⟼d∈Atoms⁡k⟼f∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdilN classDil
1 vk setvark
2 cvv classV
3 vd setvard
4 catm classAtoms
5 1 cv setvark
6 5 4 cfv classAtoms⁡k
7 vf setvarf
8 cpautN classPAut
9 5 8 cfv classPAut⁡k
10 vx setvarx
11 cpsubsp classPSubSp
12 5 11 cfv classPSubSp⁡k
13 10 cv setvarx
14 cwpointsN classWAtoms
15 5 14 cfv classWAtoms⁡k
16 3 cv setvard
17 16 15 cfv classWAtoms⁡k⁡d
18 13 17 wss wffx⊆WAtoms⁡k⁡d
19 7 cv setvarf
20 13 19 cfv classf⁡x
21 20 13 wceq wfff⁡x=x
22 18 21 wi wffx⊆WAtoms⁡k⁡d→f⁡x=x
23 22 10 12 wral wff∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x
24 23 7 9 crab classf∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x
25 3 6 24 cmpt classd∈Atoms⁡k⟼f∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x
26 1 2 25 cmpt classk∈V⟼d∈Atoms⁡k⟼f∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x
27 0 26 wceq wffDil=k∈V⟼d∈Atoms⁡k⟼f∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x