Metamath Proof Explorer

Theorem pautsetN

Description: The set of projective automorphisms. (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pautset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pautset.m ⊢ 𝑀 = ( PAut ‘ 𝐾 )
Assertion pautsetN ( 𝐾 ∈ 𝐵 → 𝑀 = { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )

Proof

Step Hyp Ref Expression
1 pautset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
2 pautset.m ⊢ 𝑀 = ( PAut ‘ 𝐾 )
3 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
4 fveq2 ⊢ ( 𝑘 = 𝐾 → ( PSubSp ‘ 𝑘 ) = ( PSubSp ‘ 𝐾 ) )
5 4 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( PSubSp ‘ 𝑘 ) = 𝑆 )
6 5 f1oeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ↔ 𝑓 : 𝑆 –1-1-onto→ ( PSubSp ‘ 𝑘 ) ) )
7 f1oeq3 ⊢ ( ( PSubSp ‘ 𝑘 ) = 𝑆 → ( 𝑓 : 𝑆 –1-1-onto→ ( PSubSp ‘ 𝑘 ) ↔ 𝑓 : 𝑆 –1-1-onto→ 𝑆 ) )
8 5 7 syl ⊢ ( 𝑘 = 𝐾 → ( 𝑓 : 𝑆 –1-1-onto→ ( PSubSp ‘ 𝑘 ) ↔ 𝑓 : 𝑆 –1-1-onto→ 𝑆 ) )
9 6 8 bitrd ⊢ ( 𝑘 = 𝐾 → ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ↔ 𝑓 : 𝑆 –1-1-onto→ 𝑆 ) )
10 5 raleqdv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) )
11 5 10 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) )
12 9 11 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) ) )
13 12 abbidv ⊢ ( 𝑘 = 𝐾 → { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )
14 df-pautN ⊢ PAut = ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )
15 1 fvexi ⊢ 𝑆 ∈ V
16 15 15 mapval ⊢ ( 𝑆 ↑m 𝑆 ) = { 𝑓 ∣ 𝑓 : 𝑆 ⟶ 𝑆 }
17 ovex ⊢ ( 𝑆 ↑m 𝑆 ) ∈ V
18 16 17 eqeltrri ⊢ { 𝑓 ∣ 𝑓 : 𝑆 ⟶ 𝑆 } ∈ V
19 f1of ⊢ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 → 𝑓 : 𝑆 ⟶ 𝑆 )
20 19 ss2abi ⊢ { 𝑓 ∣ 𝑓 : 𝑆 –1-1-onto→ 𝑆 } ⊆ { 𝑓 ∣ 𝑓 : 𝑆 ⟶ 𝑆 }
21 18 20 ssexi ⊢ { 𝑓 ∣ 𝑓 : 𝑆 –1-1-onto→ 𝑆 } ∈ V
22 simpl ⊢ ( ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 : 𝑆 –1-1-onto→ 𝑆 )
23 22 ss2abi ⊢ { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ { 𝑓 ∣ 𝑓 : 𝑆 –1-1-onto→ 𝑆 }
24 21 23 ssexi ⊢ { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
25 13 14 24 fvmpt ⊢ ( 𝐾 ∈ V → ( PAut ‘ 𝐾 ) = { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )
26 2 25 syl5eq ⊢ ( 𝐾 ∈ V → 𝑀 = { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )
27 3 26 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝑀 = { 𝑓 ∣ ( 𝑓 : 𝑆 –1-1-onto→ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )