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 ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdilN class Dil
1 vk setvar k
2 cvv class V
3 vd setvar d
4 catm class Atoms
5 1 cv setvar k
6 5 4 cfv class Atoms ⁡ k
7 vf setvar f
8 cpautN class PAut
9 5 8 cfv class PAut ⁡ k
10 vx setvar x
11 cpsubsp class PSubSp
12 5 11 cfv class PSubSp ⁡ k
13 10 cv setvar x
14 cwpointsN class WAtoms
15 5 14 cfv class WAtoms ⁡ k
16 3 cv setvar d
17 16 15 cfv class WAtoms ⁡ k ⁡ d
18 13 17 wss wff x ⊆ WAtoms ⁡ k ⁡ d
19 7 cv setvar f
20 13 19 cfv class f ⁡ x
21 20 13 wceq wff f ⁡ x = x
22 18 21 wi wff x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x
23 22 10 12 wral wff ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x
24 23 7 9 crab class f ∈ PAut ⁡ k | ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x
25 3 6 24 cmpt class d ∈ Atoms ⁡ k ⟼ f ∈ PAut ⁡ k | ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x
26 1 2 25 cmpt class k ∈ V ⟼ d ∈ Atoms ⁡ k ⟼ f ∈ PAut ⁡ k | ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x
27 0 26 wceq wff Dil = k ∈ V ⟼ d ∈ Atoms ⁡ k ⟼ f ∈ PAut ⁡ k | ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x