Definition df-pautN 38005

Description: Define set of all projective automorphisms. This is the intended definition of automorphism in [Crawley] p. 112. (Contributed by NM, 26-Jan-2012.)

Assertion

Ref	Expression
df-pautN	⊢ PAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))})

Distinct variable group:   𝑓,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-pautN

Step	Hyp	Ref	Expression
1		cpautN 38001	. 2 class PAut
2		vk	. . 3 setvar 𝑘
3		cvv 3432	. . 3 class V
4	2	cv 1538	. . . . . . 7 class 𝑘
5		cpsubsp 37510	. . . . . . 7 class PSubSp
6	4, 5	cfv 6433	. . . . . 6 class (PSubSp‘𝑘)
7		vf	. . . . . . 7 setvar 𝑓
8	7	cv 1538	. . . . . 6 class 𝑓
9	6, 6, 8	wf1o 6432	. . . . 5 wff 𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘)
10		vx	. . . . . . . . . 10 setvar 𝑥
11	10	cv 1538	. . . . . . . . 9 class 𝑥
12		vy	. . . . . . . . . 10 setvar 𝑦
13	12	cv 1538	. . . . . . . . 9 class 𝑦
14	11, 13	wss 3887	. . . . . . . 8 wff 𝑥 ⊆ 𝑦
15	11, 8	cfv 6433	. . . . . . . . 9 class (𝑓‘𝑥)
16	13, 8	cfv 6433	. . . . . . . . 9 class (𝑓‘𝑦)
17	15, 16	wss 3887	. . . . . . . 8 wff (𝑓‘𝑥) ⊆ (𝑓‘𝑦)
18	14, 17	wb 205	. . . . . . 7 wff (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦))
19	18, 12, 6	wral 3064	. . . . . 6 wff ∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦))
20	19, 10, 6	wral 3064	. . . . 5 wff ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦))
21	9, 20	wa 396	. . . 4 wff (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))
22	21, 7	cab 2715	. . 3 class {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))}
23	2, 3, 22	cmpt 5157	. 2 class (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))})
24	1, 23	wceq 1539	1 wff PAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))})

This definition is referenced by:  pautsetN  38112