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

Metamath Proof Explorer

Theorem fprodcllemf

Description: Finite product closure lemma. A version of fprodcllem using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodcllemf.ph ⊢ Ⅎ k φ
fprodcllemf.s ⊢ φ → S ⊆ ℂ
fprodcllemf.xy ⊢ φ ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
fprodcllemf.a ⊢ φ → A ∈ Fin
fprodcllemf.b ⊢ φ ∧ k ∈ A → B ∈ S
fprodcllemf.1 ⊢ φ → 1 ∈ S
Assertion fprodcllemf ⊢ φ → ∏ k ∈ A B ∈ S

Proof

Step Hyp Ref Expression
1 fprodcllemf.ph ⊢ Ⅎ k φ
2 fprodcllemf.s ⊢ φ → S ⊆ ℂ
3 fprodcllemf.xy ⊢ φ ∧ x ∈ S ∧ y ∈ S → x ⁢ y ∈ S
4 fprodcllemf.a ⊢ φ → A ∈ Fin
5 fprodcllemf.b ⊢ φ ∧ k ∈ A → B ∈ S
6 fprodcllemf.1 ⊢ φ → 1 ∈ S
7 nfcv ⊢ Ⅎ _ j B
8 nfcsb1v ⊢ Ⅎ _ k ⦋ j / k⦌ B
9 csbeq1a ⊢ k = j → B = ⦋ j / k⦌ B
10 7 8 9 cbvprodi ⊢ ∏ k ∈ A B = ∏ j ∈ A ⦋ j / k⦌ B
11 5 ex ⊢ φ → k ∈ A → B ∈ S
12 1 11 ralrimi ⊢ φ → ∀ k ∈ A B ∈ S
13 rspsbc ⊢ j ∈ A → ∀ k ∈ A B ∈ S → [˙j / k]˙ B ∈ S
14 12 13 mpan9 ⊢ φ ∧ j ∈ A → [˙j / k]˙ B ∈ S
15 sbcel1g ⊢ j ∈ V → [˙j / k]˙ B ∈ S ↔ ⦋ j / k⦌ B ∈ S
16 15 elv ⊢ [˙j / k]˙ B ∈ S ↔ ⦋ j / k⦌ B ∈ S
17 14 16 sylib ⊢ φ ∧ j ∈ A → ⦋ j / k⦌ B ∈ S
18 2 3 4 17 6 fprodcllem ⊢ φ → ∏ j ∈ A ⦋ j / k⦌ B ∈ S
19 10 18 eqeltrid ⊢ φ → ∏ k ∈ A B ∈ S