Metamath Proof Explorer

Theorem dilfsetN

Description: The mapping from fiducial atom to set of dilations. (Contributed by NM, 30-Jan-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 dilfsetN ⊢ K ∈ B → L = d ∈ A ⟼ 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 elex ⊢ K ∈ B → K ∈ V
7 fveq2 ⊢ k = K → Atoms ⁡ k = Atoms ⁡ K
8 7 1 eqtr4di ⊢ k = K → Atoms ⁡ k = A
9 fveq2 ⊢ k = K → PAut ⁡ k = PAut ⁡ K
10 9 4 eqtr4di ⊢ k = K → PAut ⁡ k = M
11 fveq2 ⊢ k = K → PSubSp ⁡ k = PSubSp ⁡ K
12 11 2 eqtr4di ⊢ k = K → PSubSp ⁡ k = S
13 fveq2 ⊢ k = K → WAtoms ⁡ k = WAtoms ⁡ K
14 13 3 eqtr4di ⊢ k = K → WAtoms ⁡ k = W
15 14 fveq1d ⊢ k = K → WAtoms ⁡ k ⁡ d = W ⁡ d
16 15 sseq2d ⊢ k = K → x ⊆ WAtoms ⁡ k ⁡ d ↔ x ⊆ W ⁡ d
17 16 imbi1d ⊢ k = K → x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x ↔ x ⊆ W ⁡ d → f ⁡ x = x
18 12 17 raleqbidv ⊢ k = K → ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x ↔ ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x
19 10 18 rabeqbidv ⊢ k = K → f ∈ PAut ⁡ k | ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x = f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x
20 8 19 mpteq12dv ⊢ k = K → d ∈ Atoms ⁡ k ⟼ f ∈ PAut ⁡ k | ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x = d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x
21 df-dilN ⊢ Dil = k ∈ V ⟼ d ∈ Atoms ⁡ k ⟼ f ∈ PAut ⁡ k | ∀ x ∈ PSubSp ⁡ k x ⊆ WAtoms ⁡ k ⁡ d → f ⁡ x = x
22 20 21 1 mptfvmpt ⊢ K ∈ V → Dil ⁡ K = d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x
23 5 22 syl5eq ⊢ K ∈ V → L = d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x
24 6 23 syl ⊢ K ∈ B → L = d ∈ A ⟼ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ d → f ⁡ x = x