This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsbascl

Description: An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt2.y ⊢ Y = S ⨉ 𝑠 x ∈ I ⟼ R
prdsbasmpt2.b ⊢ B = Base Y
prdsbasmpt2.s ⊢ φ → S ∈ V
prdsbasmpt2.i ⊢ φ → I ∈ W
prdsbasmpt2.r ⊢ φ → ∀ x ∈ I R ∈ X
prdsbasmpt2.k ⊢ K = Base R
prdsbascl.f ⊢ φ → F ∈ B
Assertion prdsbascl ⊢ φ → ∀ x ∈ I F ⁡ x ∈ K

Proof

Step Hyp Ref Expression
1 prdsbasmpt2.y ⊢ Y = S ⨉ 𝑠 x ∈ I ⟼ R
2 prdsbasmpt2.b ⊢ B = Base Y
3 prdsbasmpt2.s ⊢ φ → S ∈ V
4 prdsbasmpt2.i ⊢ φ → I ∈ W
5 prdsbasmpt2.r ⊢ φ → ∀ x ∈ I R ∈ X
6 prdsbasmpt2.k ⊢ K = Base R
7 prdsbascl.f ⊢ φ → F ∈ B
8 eqid ⊢ x ∈ I ⟼ R = x ∈ I ⟼ R
9 8 fnmpt ⊢ ∀ x ∈ I R ∈ X → x ∈ I ⟼ R Fn I
10 5 9 syl ⊢ φ → x ∈ I ⟼ R Fn I
11 1 2 3 4 10 7 prdsbasfn ⊢ φ → F Fn I
12 dffn5 ⊢ F Fn I ↔ F = x ∈ I ⟼ F ⁡ x
13 11 12 sylib ⊢ φ → F = x ∈ I ⟼ F ⁡ x
14 13 7 eqeltrrd ⊢ φ → x ∈ I ⟼ F ⁡ x ∈ B
15 1 2 3 4 5 6 prdsbasmpt2 ⊢ φ → x ∈ I ⟼ F ⁡ x ∈ B ↔ ∀ x ∈ I F ⁡ x ∈ K
16 14 15 mpbid ⊢ φ → ∀ x ∈ I F ⁡ x ∈ K