Metamath Proof Explorer

Theorem mptelixpg

Description: Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015)

Ref Expression
Assertion mptelixpg ( 𝐼 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ X 𝑥 ∈ 𝐼 𝐾 ↔ ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
2 nfcv ⊢ Ⅎ 𝑦 𝐾
3 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐾
4 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐾 = ⦋ 𝑦 / 𝑥 ⦌ 𝐾 )
5 2 3 4 cbvixp ⊢ X 𝑥 ∈ 𝐼 𝐾 = X 𝑦 ∈ 𝐼 ⦋ 𝑦 / 𝑥 ⦌ 𝐾
6 5 eleq2i ⊢ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ X 𝑥 ∈ 𝐼 𝐾 ↔ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ X 𝑦 ∈ 𝐼 ⦋ 𝑦 / 𝑥 ⦌ 𝐾 )
7 elixp2 ⊢ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ X 𝑦 ∈ 𝐼 ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V ∧ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) )
8 3anass ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V ∧ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V ∧ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) ) )
9 6 7 8 3bitri ⊢ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ X 𝑥 ∈ 𝐼 𝐾 ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V ∧ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) ) )
10 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) = ( 𝑥 ∈ 𝐼 ↦ 𝐽 )
11 10 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 )
12 10 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) = 𝐽 )
13 simpr ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾 ) → 𝐽 ∈ 𝐾 )
14 12 13 eqeltrd ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 )
15 14 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 )
16 11 15 jca ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ) )
17 dffn2 ⊢ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ↔ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) : 𝐼 ⟶ V )
18 10 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ V ↔ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) : 𝐼 ⟶ V )
19 10 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) = 𝐽 )
20 19 eleq1d ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ↔ 𝐽 ∈ 𝐾 ) )
21 20 biimpd ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 → 𝐽 ∈ 𝐾 ) )
22 21 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ V → ∀ 𝑥 ∈ 𝐼 ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 → 𝐽 ∈ 𝐾 ) )
23 ralim ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 → 𝐽 ∈ 𝐾 ) → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 → ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )
24 22 23 syl ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ V → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 → ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )
25 18 24 sylbir ⊢ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) : 𝐼 ⟶ V → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 → ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )
26 17 25 sylbi ⊢ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 → ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )
27 26 imp ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ) → ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 )
28 16 27 impbii ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ) )
29 nfv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾
30 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 )
31 30 3 nfel ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾
32 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) )
33 32 4 eleq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) )
34 29 31 33 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ↔ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 )
35 34 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) )
36 28 35 bitri ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) )
37 mptexg ⊢ ( 𝐼 ∈ V → ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V )
38 37 biantrurd ⊢ ( 𝐼 ∈ V → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V ∧ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) ) ) )
39 36 38 syl5rbb ⊢ ( 𝐼 ∈ V → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V ∧ ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) Fn 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) ) ↔ ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )
40 9 39 syl5bb ⊢ ( 𝐼 ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ X 𝑥 ∈ 𝐼 𝐾 ↔ ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )
41 1 40 syl ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ X 𝑥 ∈ 𝐼 𝐾 ↔ ∀ 𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ) )