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

Metamath Proof Explorer

Theorem ixpsnval

Description: The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018)

Ref Expression
Assertion ixpsnval ⊢ X ∈ V → ⨉ x ∈ X B = f | f Fn X ∧ f ⁡ X ∈ ⦋ X / x⦌ B

Proof

Step Hyp Ref Expression
1 dfixp ⊢ ⨉ x ∈ X B = f | f Fn X ∧ ∀ x ∈ X f ⁡ x ∈ B
2 ralsnsg ⊢ X ∈ V → ∀ x ∈ X f ⁡ x ∈ B ↔ [˙X / x]˙ f ⁡ x ∈ B
3 sbcel12 ⊢ [˙X / x]˙ f ⁡ x ∈ B ↔ ⦋ X / x⦌ f ⁡ x ∈ ⦋ X / x⦌ B
4 csbfv2g ⊢ X ∈ V → ⦋ X / x⦌ f ⁡ x = f ⁡ ⦋ X / x⦌ x
5 csbvarg ⊢ X ∈ V → ⦋ X / x⦌ x = X
6 5 fveq2d ⊢ X ∈ V → f ⁡ ⦋ X / x⦌ x = f ⁡ X
7 4 6 eqtrd ⊢ X ∈ V → ⦋ X / x⦌ f ⁡ x = f ⁡ X
8 7 eleq1d ⊢ X ∈ V → ⦋ X / x⦌ f ⁡ x ∈ ⦋ X / x⦌ B ↔ f ⁡ X ∈ ⦋ X / x⦌ B
9 3 8 bitrid ⊢ X ∈ V → [˙X / x]˙ f ⁡ x ∈ B ↔ f ⁡ X ∈ ⦋ X / x⦌ B
10 2 9 bitrd ⊢ X ∈ V → ∀ x ∈ X f ⁡ x ∈ B ↔ f ⁡ X ∈ ⦋ X / x⦌ B
11 10 anbi2d ⊢ X ∈ V → f Fn X ∧ ∀ x ∈ X f ⁡ x ∈ B ↔ f Fn X ∧ f ⁡ X ∈ ⦋ X / x⦌ B
12 11 abbidv ⊢ X ∈ V → f | f Fn X ∧ ∀ x ∈ X f ⁡ x ∈ B = f | f Fn X ∧ f ⁡ X ∈ ⦋ X / x⦌ B
13 1 12 eqtrid ⊢ X ∈ V → ⨉ x ∈ X B = f | f Fn X ∧ f ⁡ X ∈ ⦋ X / x⦌ B