Theorem mptelixpg 8885

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

Assertion

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

Distinct variable group:   𝑥,𝐼

Allowed substitution hints:   𝐽(𝑥)   𝐾(𝑥)   𝑉(𝑥)

Proof of Theorem mptelixpg

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3463	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ V)
2		nfcv 2899	. . . . . 6 ⊢ Ⅎ𝑦𝐾
3		nfcsb1v 3875	. . . . . 6 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐾
4		csbeq1a 3865	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝐾 = ⦋𝑦 / 𝑥⦌𝐾)
5	2, 3, 4	cbvixp 8864	. . . . 5 ⊢ X𝑥 ∈ 𝐼 𝐾 = X𝑦 ∈ 𝐼 ⦋𝑦 / 𝑥⦌𝐾
6	5	eleq2i 2829	. . . 4 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑦 ∈ 𝐼 ⦋𝑦 / 𝑥⦌𝐾)
7		elixp2 8851	. . . 4 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑦 ∈ 𝐼 ⦋𝑦 / 𝑥⦌𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
8		3anass 1095	. . . 4 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾) ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)))
9	6, 7, 8	3bitri 297	. . 3 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)))
10		eqid 2737	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐼 ↦ 𝐽) = (𝑥 ∈ 𝐼 ↦ 𝐽)
11	10	fnmpt 6640	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → (𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼)
12	10	fvmpt2 6961	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾) → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) = 𝐽)
13		simpr 484	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾) → 𝐽 ∈ 𝐾)
14	12, 13	eqeltrd 2837	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾) → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾)
15	14	ralimiaa 3074	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾)
16	11, 15	jca 511	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾))
17		dffn2 6672	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ↔ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶V)
18	10	fmpt 7064	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ V ↔ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶V)
19	10	fvmpt2 6961	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V) → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) = 𝐽)
20	19	eleq1d 2822	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V) → (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 ↔ 𝐽 ∈ 𝐾))
21	20	biimpd 229	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V) → (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → 𝐽 ∈ 𝐾))
22	21	ralimiaa 3074	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ V → ∀𝑥 ∈ 𝐼 (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → 𝐽 ∈ 𝐾))
23		ralim 3078	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐼 (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → 𝐽 ∈ 𝐾) → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
24	22, 23	syl 17	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ V → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
25	18, 24	sylbir 235	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶V → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
26	17, 25	sylbi 217	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
27	26	imp 406	. . . . . 6 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾) → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾)
28	16, 27	impbii 209	. . . . 5 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾))
29		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾
30		nffvmpt1 6853	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦)
31	30, 3	nfel 2914	. . . . . . 7 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾
32		fveq2 6842	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) = ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦))
33	32, 4	eleq12d 2831	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
34	29, 31, 33	cbvralw 3280	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 ↔ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)
35	34	anbi2i 624	. . . . 5 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾) ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
36	28, 35	bitri 275	. . . 4 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
37		mptexg 7177	. . . . 5 ⊢ (𝐼 ∈ V → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V)
38	37	biantrurd 532	. . . 4 ⊢ (𝐼 ∈ V → (((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾) ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))))
39	36, 38	bitr2id 284	. . 3 ⊢ (𝐼 ∈ V → (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)) ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
40	9, 39	bitrid 283	. 2 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
41	1, 40	syl 17	1 ⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114  ∀wral 3052  Vcvv 3442  ⦋csb 3851   ↦ cmpt 5181   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  Xcixp 8847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ixp 8848

This theorem is referenced by:  resixpfo  8886  ixpiunwdom  9507  dfac9  10059  prdsbasmpt  17402  prdsbasmpt2  17414  idfucl  17817  fuccocl  17903  fucidcl  17904  invfuc  17913  curf2cl  18166  yonedalem4c  18212  dprdwd  19954  ptpjopn  23568  dfac14lem  23573  ptcnplem  23577  ptcnp  23578  ptcn  23583  ptcmplem2  24009  tmdgsum2  24052  upixp  37969  kelac1  43409