elptr2

Description: A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

	Ref	Expression
Hypotheses	ptbas.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
	elptr2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	elptr2.2	⊢ ( 𝜑 → 𝑊 ∈ Fin )
	elptr2.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) )
	elptr2.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝑆 = ∪ ( 𝐹 ‘ 𝑘 ) )
Assertion	elptr2	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 𝑆 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ptbas.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2		elptr2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		elptr2.2	⊢ ( 𝜑 → 𝑊 ∈ Fin )
4		elptr2.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) )
5		elptr2.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝑆 = ∪ ( 𝐹 ‘ 𝑘 ) )
6		nffvmpt1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 )
7		nfcv	⊢ Ⅎ 𝑦 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 )
8		fveq2	⊢ ( 𝑦 = 𝑘 → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) )
9	6 7 8	cbvixp	⊢ X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = X 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
11		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑆 )
12	11	fvmpt2	⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = 𝑆 )
13	10 4 12	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = 𝑆 )
14	13	ixpeq2dva	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝐴 𝑆 )
15	9 14	syl5eq	⊢ ( 𝜑 → X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = X 𝑘 ∈ 𝐴 𝑆 )
16	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) )
17	11	fnmpt	⊢ ( ∀ 𝑘 ∈ 𝐴 𝑆 ∈ ( 𝐹 ‘ 𝑘 ) → ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) Fn 𝐴 )
18	16 17	syl	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) Fn 𝐴 )
19	13 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
20	19	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
21	6	nfel1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 )
22		nfv	⊢ Ⅎ 𝑦 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 )
23		fveq2	⊢ ( 𝑦 = 𝑘 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑘 ) )
24	8 23	eleq12d	⊢ ( 𝑦 = 𝑘 → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) )
25	21 22 24	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
26	20 25	sylibr	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) )
27		eldifi	⊢ ( 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) → 𝑘 ∈ 𝐴 )
28	27 13	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = 𝑆 )
29	28 5	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
30	29	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
31	6	nfeq1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 )
32		nfv	⊢ Ⅎ 𝑦 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
33	23	unieqd	⊢ ( 𝑦 = 𝑘 → ∪ ( 𝐹 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
34	8 33	eqeq12d	⊢ ( 𝑦 = 𝑘 → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) )
35	31 32 34	cbvralw	⊢ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
36	30 35	sylibr	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) )
37	1	elptr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑊 ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑊 ) ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ 𝐵 )
38	2 18 26 3 36 37	syl122anc	⊢ ( 𝜑 → X 𝑦 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑦 ) ∈ 𝐵 )
39	15 38	eqeltrrd	⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 𝑆 ∈ 𝐵 )

Metamath Proof Explorer

Theorem elptr2

Proof