Metamath Proof Explorer

Theorem ispautN

Description: The predictate "is a projective automorphism." (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pautset.s ⊢ S = PSubSp ⁡ K
pautset.m ⊢ M = PAut ⁡ K
Assertion ispautN ⊢ K ∈ B → F ∈ M ↔ F : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ F ⁡ x ⊆ F ⁡ y

Proof

Step Hyp Ref Expression
1 pautset.s ⊢ S = PSubSp ⁡ K
2 pautset.m ⊢ M = PAut ⁡ K
3 1 2 pautsetN ⊢ K ∈ B → M = f | f : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
4 3 eleq2d ⊢ K ∈ B → F ∈ M ↔ F ∈ f | f : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y
5 f1of ⊢ F : S ⟶ 1-1 onto S → F : S ⟶ S
6 1 fvexi ⊢ S ∈ V
7 fex ⊢ F : S ⟶ S ∧ S ∈ V → F ∈ V
8 5 6 7 sylancl ⊢ F : S ⟶ 1-1 onto S → F ∈ V
9 8 adantr ⊢ F : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ F ⁡ x ⊆ F ⁡ y → F ∈ V
10 f1oeq1 ⊢ f = F → f : S ⟶ 1-1 onto S ↔ F : S ⟶ 1-1 onto S
11 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
12 fveq1 ⊢ f = F → f ⁡ y = F ⁡ y
13 11 12 sseq12d ⊢ f = F → f ⁡ x ⊆ f ⁡ y ↔ F ⁡ x ⊆ F ⁡ y
14 13 bibi2d ⊢ f = F → x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y ↔ x ⊆ y ↔ F ⁡ x ⊆ F ⁡ y
15 14 2ralbidv ⊢ f = F → ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y ↔ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ F ⁡ x ⊆ F ⁡ y
16 10 15 anbi12d ⊢ f = F → f : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y ↔ F : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ F ⁡ x ⊆ F ⁡ y
17 9 16 elab3 ⊢ F ∈ f | f : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ f ⁡ x ⊆ f ⁡ y ↔ F : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ F ⁡ x ⊆ F ⁡ y
18 4 17 bitrdi ⊢ K ∈ B → F ∈ M ↔ F : S ⟶ 1-1 onto S ∧ ∀ x ∈ S ∀ y ∈ S x ⊆ y ↔ F ⁡ x ⊆ F ⁡ y