Theorem ptval

Description: The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015)

	Ref	Expression
Hypothesis	ptval.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
Assertion	ptval	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ptval.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
2		df-pt	⊢ ∏t = ( 𝑓 ∈ V ↦ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } ) )
3		simpr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
4	3	dmeqd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = dom 𝐹 )
5		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6	5	ad2antlr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝐹 = 𝐴 )
7	4 6	eqtrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = 𝐴 )
8	7	fneq2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑔 Fn dom 𝑓 ↔ 𝑔 Fn 𝐴 ) )
9	3	fveq1d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
10	9	eleq2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
11	7 10	raleqbidv	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
12	7	difeq1d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( dom 𝑓 ∖ 𝑧 ) = ( 𝐴 ∖ 𝑧 ) )
13	9	unieqd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ∪ ( 𝑓 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) )
14	13	eqeq2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
15	12 14	raleqbidv	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
16	15	rexbidv	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) )
17	8 11 16	3anbi123d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) )
18	7	ixpeq1d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
19	18	eqeq2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ↔ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) )
20	17 19	anbi12d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) ↔ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) )
21	20	exbidv	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) )
22	21	abbidv	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } )
23	22 1	eqtr4di	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } = 𝐵 )
24	23	fveq2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } ) = ( topGen ‘ 𝐵 ) )
25		fnex	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
26	25	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → 𝐹 ∈ V )
27		fvexd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → ( topGen ‘ 𝐵 ) ∈ V )
28	2 24 26 27	fvmptd2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ 𝐵 ) )