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 ⊢I∈V→x∈I⟼J∈⨉x∈IK↔∀x∈IJ∈K

Proof

Step Hyp Ref Expression
1 elex ⊢I∈V→I∈V
2 nfcv ⊢Ⅎ_yK
3 nfcsb1v ⊢Ⅎ_x⦋y/x⦌K
4 csbeq1a ⊢x=y→K=⦋y/x⦌K
5 2 3 4 cbvixp ⊢⨉x∈IK=⨉y∈I⦋y/x⦌K
6 5 eleq2i ⊢x∈I⟼J∈⨉x∈IK↔x∈I⟼J∈⨉y∈I⦋y/x⦌K
7 elixp2 ⊢x∈I⟼J∈⨉y∈I⦋y/x⦌K↔x∈I⟼J∈V∧x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K
8 3anass ⊢x∈I⟼J∈V∧x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K↔x∈I⟼J∈V∧x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K
9 6 7 8 3bitri ⊢x∈I⟼J∈⨉x∈IK↔x∈I⟼J∈V∧x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K
10 eqid ⊢x∈I⟼J=x∈I⟼J
11 10 fnmpt ⊢∀x∈IJ∈K→x∈I⟼JFnI
12 10 fvmpt2 ⊢x∈I∧J∈K→x∈I⟼J⁡x=J
13 simpr ⊢x∈I∧J∈K→J∈K
14 12 13 eqeltrd ⊢x∈I∧J∈K→x∈I⟼J⁡x∈K
15 14 ralimiaa ⊢∀x∈IJ∈K→∀x∈Ix∈I⟼J⁡x∈K
16 11 15 jca ⊢∀x∈IJ∈K→x∈I⟼JFnI∧∀x∈Ix∈I⟼J⁡x∈K
17 dffn2 ⊢x∈I⟼JFnI↔x∈I⟼J:I⟶V
18 10 fmpt ⊢∀x∈IJ∈V↔x∈I⟼J:I⟶V
19 10 fvmpt2 ⊢x∈I∧J∈V→x∈I⟼J⁡x=J
20 19 eleq1d ⊢x∈I∧J∈V→x∈I⟼J⁡x∈K↔J∈K
21 20 biimpd ⊢x∈I∧J∈V→x∈I⟼J⁡x∈K→J∈K
22 21 ralimiaa ⊢∀x∈IJ∈V→∀x∈Ix∈I⟼J⁡x∈K→J∈K
23 ralim ⊢∀x∈Ix∈I⟼J⁡x∈K→J∈K→∀x∈Ix∈I⟼J⁡x∈K→∀x∈IJ∈K
24 22 23 syl ⊢∀x∈IJ∈V→∀x∈Ix∈I⟼J⁡x∈K→∀x∈IJ∈K
25 18 24 sylbir ⊢x∈I⟼J:I⟶V→∀x∈Ix∈I⟼J⁡x∈K→∀x∈IJ∈K
26 17 25 sylbi ⊢x∈I⟼JFnI→∀x∈Ix∈I⟼J⁡x∈K→∀x∈IJ∈K
27 26 imp ⊢x∈I⟼JFnI∧∀x∈Ix∈I⟼J⁡x∈K→∀x∈IJ∈K
28 16 27 impbii ⊢∀x∈IJ∈K↔x∈I⟼JFnI∧∀x∈Ix∈I⟼J⁡x∈K
29 nfv ⊢Ⅎyx∈I⟼J⁡x∈K
30 nffvmpt1 ⊢Ⅎ_xx∈I⟼J⁡y
31 30 3 nfel ⊢Ⅎxx∈I⟼J⁡y∈⦋y/x⦌K
32 fveq2 ⊢x=y→x∈I⟼J⁡x=x∈I⟼J⁡y
33 32 4 eleq12d ⊢x=y→x∈I⟼J⁡x∈K↔x∈I⟼J⁡y∈⦋y/x⦌K
34 29 31 33 cbvralw ⊢∀x∈Ix∈I⟼J⁡x∈K↔∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K
35 34 anbi2i ⊢x∈I⟼JFnI∧∀x∈Ix∈I⟼J⁡x∈K↔x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K
36 28 35 bitri ⊢∀x∈IJ∈K↔x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K
37 mptexg ⊢I∈V→x∈I⟼J∈V
38 37 biantrurd ⊢I∈V→x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K↔x∈I⟼J∈V∧x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K
39 36 38 bitr2id ⊢I∈V→x∈I⟼J∈V∧x∈I⟼JFnI∧∀y∈Ix∈I⟼J⁡y∈⦋y/x⦌K↔∀x∈IJ∈K
40 9 39 bitrid ⊢I∈V→x∈I⟼J∈⨉x∈IK↔∀x∈IJ∈K
41 1 40 syl ⊢I∈V→x∈I⟼J∈⨉x∈IK↔∀x∈IJ∈K