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 I K x I J K

Proof

Step Hyp Ref Expression
1 elex I V I V
2 nfcv _ y K
3 nfcsb1v _ x y / x K
4 csbeq1a x = y K = y / x K
5 2 3 4 cbvixp x I K = y I y / x K
6 5 eleq2i x I J x I K x I J y I y / x K
7 elixp2 x I J y I y / x K x I J V x I J Fn I y I x I J y y / x K
8 3anass x I J V x I J Fn I y I x I J y y / x K x I J V x I J Fn I y I x I J y y / x K
9 6 7 8 3bitri x I J x I K x I J V x I J Fn I y I x I J y y / x K
10 eqid x I J = x I J
11 10 fnmpt x I J K x I J Fn I
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 I J K x I x I J x K
16 11 15 jca x I J K x I J Fn I x I x I J x K
17 dffn2 x I J Fn I x I J : I V
18 10 fmpt x I J 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 I J V x I x I J x K J K
23 ralim x I x I J x K J K x I x I J x K x I J K
24 22 23 syl x I J V x I x I J x K x I J K
25 18 24 sylbir x I J : I V x I x I J x K x I J K
26 17 25 sylbi x I J Fn I x I x I J x K x I J K
27 26 imp x I J Fn I x I x I J x K x I J K
28 16 27 impbii x I J K x I J Fn I x I x I J x K
29 nfv y x I J x K
30 nffvmpt1 _ x x I J y
31 30 3 nfel x x 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 I x I J x K y I x I J y y / x K
35 34 anbi2i x I J Fn I x I x I J x K x I J Fn I y I x I J y y / x K
36 28 35 bitri x I J K x I J Fn I y I x I J y y / x K
37 mptexg I V x I J V
38 37 biantrurd I V x I J Fn I y I x I J y y / x K x I J V x I J Fn I y I x I J y y / x K
39 36 38 bitr2id I V x I J V x I J Fn I y I x I J y y / x K x I J K
40 9 39 bitrid I V x I J x I K x I J K
41 1 40 syl I V x I J x I K x I J K