Metamath Proof Explorer

Theorem dilsetN

Description: The set of dilations for a fiducial atom D . (Contributed by NM, 4-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses dilset.a ⊢ A = Atoms ⁡ K
dilset.s ⊢ S = PSubSp ⁡ K
dilset.w ⊢ W = WAtoms ⁡ K
dilset.m ⊢ M = PAut ⁡ K
dilset.l ⊢ L = Dil ⁡ K
Assertion dilsetN ⊢ K ∈ B ∧ D ∈ A → L ⁡ D = f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x

Proof

Step Hyp Ref Expression
1 dilset.a ⊢ A = Atoms ⁡ K
2 dilset.s ⊢ S = PSubSp ⁡ K
3 dilset.w ⊢ W = WAtoms ⁡ K
4 dilset.m ⊢ M = PAut ⁡ K
5 dilset.l ⊢ L = Dil ⁡ K
6 1 2 3 4 5 dilfsetN ⊢ K ∈ B → L = d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x
7 6 fveq1d ⊢ K ∈ B → L ⁡ D = d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x ⁡ D
8 fveq2 ⊢ d = D → W ⁡ d = W ⁡ D
9 8 sseq2d ⊢ d = D → x ⊆ W ⁡ d ↔ x ⊆ W ⁡ D
10 9 imbi1d ⊢ d = D → x ⊆ W ⁡ d → f ⁡ x = x ↔ x ⊆ W ⁡ D → f ⁡ x = x
11 10 ralbidv ⊢ d = D → ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x ↔ ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x
12 11 rabbidv ⊢ d = D → f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x = f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x
13 eqid ⊢ d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x = d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x
14 4 fvexi ⊢ M ∈ V
15 14 rabex ⊢ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x ∈ V
16 12 13 15 fvmpt ⊢ D ∈ A → d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x ⁡ D = f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x
17 7 16 sylan9eq ⊢ K ∈ B ∧ D ∈ A → L ⁡ D = f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x