Metamath Proof Explorer

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 = k ∈ V ⟼ f | f : PSubSp ⁡ k ⟶ 1-1 onto PSubSp ⁡ k ∧ ∀ x ∈ PSubSp ⁡ k ∀ y ∈ PSubSp ⁡ k x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpautN class PAut
1 vk setvar k
2 cvv class V
3 vf setvar f
4 3 cv setvar f
5 cpsubsp class PSubSp
6 1 cv setvar k
7 6 5 cfv class PSubSp ⁡ k
8 7 7 4 wf1o wff f : PSubSp ⁡ k ⟶ 1-1 onto PSubSp ⁡ k
9 vx setvar x
10 vy setvar y
11 9 cv setvar x
12 10 cv setvar y
13 11 12 wss wff x ⊆ y
14 11 4 cfv class f ⁡ x
15 12 4 cfv class f ⁡ y
16 14 15 wss wff f ⁡ x ⊆ f ⁡ y
17 13 16 wb wff x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
18 17 10 7 wral wff ∀ y ∈ PSubSp ⁡ k x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
19 18 9 7 wral wff ∀ x ∈ PSubSp ⁡ k ∀ y ∈ PSubSp ⁡ k x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
20 8 19 wa wff f : PSubSp ⁡ k ⟶ 1-1 onto PSubSp ⁡ k ∧ ∀ x ∈ PSubSp ⁡ k ∀ y ∈ PSubSp ⁡ k x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
21 20 3 cab class f | f : PSubSp ⁡ k ⟶ 1-1 onto PSubSp ⁡ k ∧ ∀ x ∈ PSubSp ⁡ k ∀ y ∈ PSubSp ⁡ k x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
22 1 2 21 cmpt class k ∈ V ⟼ f | f : PSubSp ⁡ k ⟶ 1-1 onto PSubSp ⁡ k ∧ ∀ x ∈ PSubSp ⁡ k ∀ y ∈ PSubSp ⁡ k x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
23 0 22 wceq wff PAut = k ∈ V ⟼ f | f : PSubSp ⁡ k ⟶ 1-1 onto PSubSp ⁡ k ∧ ∀ x ∈ PSubSp ⁡ k ∀ y ∈ PSubSp ⁡ k x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y