Definition df-pautN

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpautN	⊢ PAut
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vf	⊢ 𝑓
4	3	cv	⊢ 𝑓
5		cpsubsp	⊢ PSubSp
6	1	cv	⊢ 𝑘
7	6 5	cfv	⊢ ( PSubSp ‘ 𝑘 )
8	7 7 4	wf1o	⊢ 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 )
9		vx	⊢ 𝑥
10		vy	⊢ 𝑦
11	9	cv	⊢ 𝑥
12	10	cv	⊢ 𝑦
13	11 12	wss	⊢ 𝑥 ⊆ 𝑦
14	11 4	cfv	⊢ ( 𝑓 ‘ 𝑥 )
15	12 4	cfv	⊢ ( 𝑓 ‘ 𝑦 )
16	14 15	wss	⊢ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 )
17	13 16	wb	⊢ ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) )
18	17 10 7	wral	⊢ ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) )
19	18 9 7	wral	⊢ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) )
20	8 19	wa	⊢ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
21	20 3	cab	⊢ { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) }
22	1 2 21	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )
23	0 22	wceq	⊢ PAut = ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )