Theorem mptelixpg 8941

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 3471	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ V)
2		nfcv 2922	. . . . . 6 ⊢ Ⅎ𝑦𝐾
3		nfcsb1v 3870	. . . . . 6 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐾
4		csbeq1a 3860	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝐾 = ⦋𝑦 / 𝑥⦌𝐾)
5	2, 3, 4	cbvixp 8920	. . . . 5 ⊢ X𝑥 ∈ 𝐼 𝐾 = X𝑦 ∈ 𝐼 ⦋𝑦 / 𝑥⦌𝐾
6	5	eleq2i 2852	. . . 4 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑦 ∈ 𝐼 ⦋𝑦 / 𝑥⦌𝐾)
7		elixp2 8907	. . . 4 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑦 ∈ 𝐼 ⦋𝑦 / 𝑥⦌𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
8		3anass 1111	. . . 4 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾) ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)))
9	6, 7, 8	3bitri 300	. . 3 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)))
10		eqid 2760	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐼 ↦ 𝐽) = (𝑥 ∈ 𝐼 ↦ 𝐽)
11	10	fnmpt 6667	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → (𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼)
12	10	fvmpt2 6993	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾) → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) = 𝐽)
13		simpr 490	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾) → 𝐽 ∈ 𝐾)
14	12, 13	eqeltrd 2860	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ 𝐾) → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾)
15	14	ralimiaa 3098	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾)
16	11, 15	jca 521	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 → ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾))
17		dffn2 6699	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ↔ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶V)
18	10	fmpt 7098	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ V ↔ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶V)
19	10	fvmpt2 6993	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V) → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) = 𝐽)
20	19	eleq1d 2845	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V) → (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 ↔ 𝐽 ∈ 𝐾))
21	20	biimpd 232	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐼 ∧ 𝐽 ∈ V) → (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → 𝐽 ∈ 𝐾))
22	21	ralimiaa 3098	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ V → ∀𝑥 ∈ 𝐼 (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → 𝐽 ∈ 𝐾))
23		ralim 3102	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐼 (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → 𝐽 ∈ 𝐾) → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
24	22, 23	syl 18	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ V → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
25	18, 24	sylbir 238	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶V → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
26	17, 25	sylbi 220	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 → (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
27	26	imp 412	. . . . . 6 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾) → ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾)
28	16, 27	impbii 212	. . . . 5 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾))
29		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾
30		nffvmpt1 6884	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦)
31	30, 3	nfel 2936	. . . . . . 7 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾
32		fveq2 6873	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) = ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦))
33	32, 4	eleq12d 2854	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
34	29, 31, 33	cbvralw 3304	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾 ↔ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)
35	34	anbi2i 635	. . . . 5 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑥) ∈ 𝐾) ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
36	28, 35	bitri 278	. . . 4 ⊢ (∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾 ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))
37		mptexg 7215	. . . . 5 ⊢ (𝐼 ∈ V → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V)
38	37	biantrurd 542	. . . 4 ⊢ (𝐼 ∈ V → (((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾) ↔ ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾))))
39	36, 38	bitr2id 287	. . 3 ⊢ (𝐼 ∈ V → (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ ((𝑥 ∈ 𝐼 ↦ 𝐽) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((𝑥 ∈ 𝐼 ↦ 𝐽)‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝐾)) ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
40	9, 39	bitrid 286	. 2 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
41	1, 40	syl 18	1 ⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145  ∀wral 3076  Vcvv 3450  ⦋csb 3846   ↦ cmpt 5185   Fn wfn 6522  ⟶wf 6523  ‘cfv 6527  Xcixp 8903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ixp 8904

This theorem is used by:  resixpfo  8942  ixpiunwdom  9562  dfac9  10187  prdsbasmpt  17603  prdsbasmpt2  17615  idfucl  18018  fuccocl  18104  fucidcl  18105  invfuc  18114  curf2cl  18367  yonedalem4c  18413  dprdwd  20189  ptpjopn  23893  dfac14lem  23898  ptcnplem  23902  ptcnp  23903  ptcn  23908  ptcmplem2  24334  tmdgsum2  24377  upixp  38583  kelac1  44008