ptpconn

Description: The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

		Ref	Expression
	Assertion	ptpconn	$⊢ (A \in V \land F : A ⟶ PConn) \to \prod_{𝑡} (F) \in PConn$

Proof

Step	Hyp	Ref	Expression
1		pconntop	$⊢ x \in PConn \to x \in Top$
2	1	ssriv	$⊢ PConn \subseteq Top$
3		fss	$⊢ (F : A ⟶ PConn \land PConn \subseteq Top) \to F : A ⟶ Top$
4	2 3	mpan2	$⊢ F : A ⟶ PConn \to F : A ⟶ Top$
5		pttop	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) \in Top$
6	4 5	sylan2	$⊢ (A \in V \land F : A ⟶ PConn) \to \prod_{𝑡} (F) \in Top$
7		fvex	$⊢ I (A) \in V$
8		ovex	$⊢ II Cn F (i) \in V$
9	7 8	iunex	$⊢ ⋃_{i \in I (A)} (II Cn F (i)) \in V$
10		fvi	$⊢ A \in V \to I (A) = A$
11	10	ad2antrr	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to I (A) = A$
12	11	eleq2d	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (t \in I (A) \leftrightarrow t \in A)$
13		simplr	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to F : A ⟶ PConn$
14	13	ffvelcdmda	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land t \in A) \to F (t) \in PConn$
15		simprl	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x \in ⋃ \prod_{𝑡} (F)$
16		eqid	$⊢ \prod_{𝑡} (F) = \prod_{𝑡} (F)$
17	16	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{t \in A}{⨉} ⋃ F (t) = ⋃ \prod_{𝑡} (F)$
18	4 17	sylan2	$⊢ (A \in V \land F : A ⟶ PConn) \to \underset{t \in A}{⨉} ⋃ F (t) = ⋃ \prod_{𝑡} (F)$
19	18	adantr	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \underset{t \in A}{⨉} ⋃ F (t) = ⋃ \prod_{𝑡} (F)$
20	15 19	eleqtrrd	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x \in \underset{t \in A}{⨉} ⋃ F (t)$
21		vex	$⊢ x \in V$
22	21	elixp	$⊢ x \in \underset{t \in A}{⨉} ⋃ F (t) \leftrightarrow (x Fn A \land \forall t \in A x (t) \in ⋃ F (t))$
23	20 22	sylib	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (x Fn A \land \forall t \in A x (t) \in ⋃ F (t))$
24	23	simprd	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \forall t \in A x (t) \in ⋃ F (t)$
25	24	r19.21bi	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land t \in A) \to x (t) \in ⋃ F (t)$
26		simprr	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y \in ⋃ \prod_{𝑡} (F)$
27	26 19	eleqtrrd	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y \in \underset{t \in A}{⨉} ⋃ F (t)$
28		vex	$⊢ y \in V$
29	28	elixp	$⊢ y \in \underset{t \in A}{⨉} ⋃ F (t) \leftrightarrow (y Fn A \land \forall t \in A y (t) \in ⋃ F (t))$
30	27 29	sylib	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (y Fn A \land \forall t \in A y (t) \in ⋃ F (t))$
31	30	simprd	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \forall t \in A y (t) \in ⋃ F (t)$
32	31	r19.21bi	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land t \in A) \to y (t) \in ⋃ F (t)$
33		eqid	$⊢ ⋃ F (t) = ⋃ F (t)$
34	33	pconncn	$⊢ (F (t) \in PConn \land x (t) \in ⋃ F (t) \land y (t) \in ⋃ F (t)) \to \exists f \in (II Cn F (t)) (f (0) = x (t) \land f (1) = y (t))$
35	14 25 32 34	syl3anc	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land t \in A) \to \exists f \in (II Cn F (t)) (f (0) = x (t) \land f (1) = y (t))$
36		df-rex	$⊢ \exists f \in (II Cn F (t)) (f (0) = x (t) \land f (1) = y (t)) \leftrightarrow \exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))$
37	35 36	sylib	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land t \in A) \to \exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))$
38	12 37	sylbida	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land t \in I (A)) \to \exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))$
39	38	ralrimiva	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \forall t \in I (A) \exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))$
40		fveq2	$⊢ i = t \to F (i) = F (t)$
41	40	oveq2d	$⊢ i = t \to II Cn F (i) = II Cn F (t)$
42	41	ssiun2s	$⊢ t \in I (A) \to II Cn F (t) \subseteq ⋃_{i \in I (A)} (II Cn F (i))$
43	42	sseld	$⊢ t \in I (A) \to (f \in (II Cn F (t)) \to f \in ⋃_{i \in I (A)} (II Cn F (i)))$
44	43	adantrd	$⊢ t \in I (A) \to ((f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))) \to f \in ⋃_{i \in I (A)} (II Cn F (i)))$
45	44	ancrd	$⊢ t \in I (A) \to ((f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))) \to (f \in ⋃_{i \in I (A)} (II Cn F (i)) \land (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))))$
46	45	eximdv	$⊢ t \in I (A) \to (\exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))) \to \exists f (f \in ⋃_{i \in I (A)} (II Cn F (i)) \land (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))))$
47		df-rex	$⊢ \exists f \in ⋃_{i \in I (A)} (II Cn F (i)) (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))) \leftrightarrow \exists f (f \in ⋃_{i \in I (A)} (II Cn F (i)) \land (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))))$
48	46 47	imbitrrdi	$⊢ t \in I (A) \to (\exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))) \to \exists f \in ⋃_{i \in I (A)} (II Cn F (i)) (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))))$
49	48	ralimia	$⊢ \forall t \in I (A) \exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))) \to \forall t \in I (A) \exists f \in ⋃_{i \in I (A)} (II Cn F (i)) (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))$
50	39 49	syl	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \forall t \in I (A) \exists f \in ⋃_{i \in I (A)} (II Cn F (i)) (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))$
51		eleq1	$⊢ f = g (t) \to (f \in (II Cn F (t)) \leftrightarrow g (t) \in (II Cn F (t)))$
52		fveq1	$⊢ f = g (t) \to f (0) = g (t) (0)$
53	52	eqeq1d	$⊢ f = g (t) \to (f (0) = x (t) \leftrightarrow g (t) (0) = x (t))$
54		fveq1	$⊢ f = g (t) \to f (1) = g (t) (1)$
55	54	eqeq1d	$⊢ f = g (t) \to (f (1) = y (t) \leftrightarrow g (t) (1) = y (t))$
56	53 55	anbi12d	$⊢ f = g (t) \to ((f (0) = x (t) \land f (1) = y (t)) \leftrightarrow (g (t) (0) = x (t) \land g (t) (1) = y (t)))$
57	51 56	anbi12d	$⊢ f = g (t) \to ((f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t))) \leftrightarrow (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))$
58	57	ac6	$⊢ (I (A) \in V \land ⋃_{i \in I (A)} (II Cn F (i)) \in V \land \forall t \in I (A) \exists f \in ⋃_{i \in I (A)} (II Cn F (i)) (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (1) = y (t)))) \to \exists g (g : I (A) ⟶ ⋃_{i \in I (A)} (II Cn F (i)) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))$
59	7 9 50 58	mp3an12i	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \exists g (g : I (A) ⟶ ⋃_{i \in I (A)} (II Cn F (i)) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))$
60		ffn	$⊢ g : I (A) ⟶ ⋃_{i \in I (A)} (II Cn F (i)) \to g Fn I (A)$
61	60	anim1i	$⊢ (g : I (A) ⟶ ⋃_{i \in I (A)} (II Cn F (i)) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t)))) \to (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))$
62	61	eximi	$⊢ \exists g (g : I (A) ⟶ ⋃_{i \in I (A)} (II Cn F (i)) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t)))) \to \exists g (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))$
63	59 62	syl	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \exists g (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))$
64		iitopon	$⊢ II \in TopOn ([0, 1])$
65	64	a1i	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to II \in TopOn ([0, 1])$
66		simplll	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to A \in V$
67	13	adantr	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to F : A ⟶ PConn$
68	67 4	syl	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to F : A ⟶ Top$
69		simprr	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t)))$
70	11	adantr	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to I (A) = A$
71	70	eleq2d	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (i \in I (A) \leftrightarrow i \in A)$
72	71	biimpar	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to i \in I (A)$
73		fveq2	$⊢ t = i \to g (t) = g (i)$
74		fveq2	$⊢ t = i \to F (t) = F (i)$
75	74	oveq2d	$⊢ t = i \to II Cn F (t) = II Cn F (i)$
76	73 75	eleq12d	$⊢ t = i \to (g (t) \in (II Cn F (t)) \leftrightarrow g (i) \in (II Cn F (i)))$
77	73	fveq1d	$⊢ t = i \to g (t) (0) = g (i) (0)$
78		fveq2	$⊢ t = i \to x (t) = x (i)$
79	77 78	eqeq12d	$⊢ t = i \to (g (t) (0) = x (t) \leftrightarrow g (i) (0) = x (i))$
80	73	fveq1d	$⊢ t = i \to g (t) (1) = g (i) (1)$
81		fveq2	$⊢ t = i \to y (t) = y (i)$
82	80 81	eqeq12d	$⊢ t = i \to (g (t) (1) = y (t) \leftrightarrow g (i) (1) = y (i))$
83	79 82	anbi12d	$⊢ t = i \to ((g (t) (0) = x (t) \land g (t) (1) = y (t)) \leftrightarrow (g (i) (0) = x (i) \land g (i) (1) = y (i)))$
84	76 83	anbi12d	$⊢ t = i \to ((g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))) \leftrightarrow (g (i) \in (II Cn F (i)) \land (g (i) (0) = x (i) \land g (i) (1) = y (i))))$
85	84	rspccva	$⊢ (\forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))) \land i \in I (A)) \to (g (i) \in (II Cn F (i)) \land (g (i) (0) = x (i) \land g (i) (1) = y (i)))$
86	69 72 85	syl2an2r	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to (g (i) \in (II Cn F (i)) \land (g (i) (0) = x (i) \land g (i) (1) = y (i)))$
87	86	simpld	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to g (i) \in (II Cn F (i))$
88		iiuni	$⊢ [0, 1] = ⋃ II$
89		eqid	$⊢ ⋃ F (i) = ⋃ F (i)$
90	88 89	cnf	$⊢ g (i) \in (II Cn F (i)) \to g (i) : [0, 1] ⟶ ⋃ F (i)$
91	87 90	syl	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to g (i) : [0, 1] ⟶ ⋃ F (i)$
92	91	feqmptd	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to g (i) = (z \in [0, 1] ⟼ g (i) (z))$
93	92 87	eqeltrrd	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to (z \in [0, 1] ⟼ g (i) (z)) \in (II Cn F (i))$
94	16 65 66 68 93	ptcn	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) \in (II Cn \prod_{𝑡} (F))$
95	86	simprd	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to (g (i) (0) = x (i) \land g (i) (1) = y (i))$
96	95	simpld	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to g (i) (0) = x (i)$
97	96	mpteq2dva	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (i \in A ⟼ g (i) (0)) = (i \in A ⟼ x (i))$
98		0elunit	$⊢ 0 \in [0, 1]$
99	66	mptexd	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (i \in A ⟼ g (i) (0)) \in V$
100		fveq2	$⊢ z = 0 \to g (i) (z) = g (i) (0)$
101	100	mpteq2dv	$⊢ z = 0 \to (i \in A ⟼ g (i) (z)) = (i \in A ⟼ g (i) (0))$
102		eqid	$⊢ (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z)))$
103	101 102	fvmptg	$⊢ (0 \in [0, 1] \land (i \in A ⟼ g (i) (0)) \in V) \to (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (0) = (i \in A ⟼ g (i) (0))$
104	98 99 103	sylancr	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (0) = (i \in A ⟼ g (i) (0))$
105	23	simpld	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x Fn A$
106	105	adantr	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to x Fn A$
107		dffn5	$⊢ x Fn A \leftrightarrow x = (i \in A ⟼ x (i))$
108	106 107	sylib	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to x = (i \in A ⟼ x (i))$
109	97 104 108	3eqtr4d	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (0) = x$
110	95	simprd	$⊢ ((((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \land i \in A) \to g (i) (1) = y (i)$
111	110	mpteq2dva	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (i \in A ⟼ g (i) (1)) = (i \in A ⟼ y (i))$
112		1elunit	$⊢ 1 \in [0, 1]$
113	66	mptexd	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (i \in A ⟼ g (i) (1)) \in V$
114		fveq2	$⊢ z = 1 \to g (i) (z) = g (i) (1)$
115	114	mpteq2dv	$⊢ z = 1 \to (i \in A ⟼ g (i) (z)) = (i \in A ⟼ g (i) (1))$
116	115 102	fvmptg	$⊢ (1 \in [0, 1] \land (i \in A ⟼ g (i) (1)) \in V) \to (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (1) = (i \in A ⟼ g (i) (1))$
117	112 113 116	sylancr	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (1) = (i \in A ⟼ g (i) (1))$
118	30	simpld	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y Fn A$
119	118	adantr	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to y Fn A$
120		dffn5	$⊢ y Fn A \leftrightarrow y = (i \in A ⟼ y (i))$
121	119 120	sylib	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to y = (i \in A ⟼ y (i))$
122	111 117 121	3eqtr4d	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (1) = y$
123		fveq1	$⊢ f = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) \to f (0) = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (0)$
124	123	eqeq1d	$⊢ f = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) \to (f (0) = x \leftrightarrow (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (0) = x)$
125		fveq1	$⊢ f = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) \to f (1) = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (1)$
126	125	eqeq1d	$⊢ f = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) \to (f (1) = y \leftrightarrow (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (1) = y)$
127	124 126	anbi12d	$⊢ f = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) \to ((f (0) = x \land f (1) = y) \leftrightarrow ((z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (0) = x \land (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (1) = y))$
128	127	rspcev	$⊢ ((z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) \in (II Cn \prod_{𝑡} (F)) \land ((z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (0) = x \land (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) (1) = y)) \to \exists f \in (II Cn \prod_{𝑡} (F)) (f (0) = x \land f (1) = y)$
129	94 109 122 128	syl12anc	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (g Fn I (A) \land \forall t \in I (A) (g (t) \in (II Cn F (t)) \land (g (t) (0) = x (t) \land g (t) (1) = y (t))))) \to \exists f \in (II Cn \prod_{𝑡} (F)) (f (0) = x \land f (1) = y)$
130	63 129	exlimddv	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \exists f \in (II Cn \prod_{𝑡} (F)) (f (0) = x \land f (1) = y)$
131	130	ralrimivva	$⊢ (A \in V \land F : A ⟶ PConn) \to \forall x \in ⋃ \prod_{𝑡} (F) \forall y \in ⋃ \prod_{𝑡} (F) \exists f \in (II Cn \prod_{𝑡} (F)) (f (0) = x \land f (1) = y)$
132		eqid	$⊢ ⋃ \prod_{𝑡} (F) = ⋃ \prod_{𝑡} (F)$
133	132	ispconn	$⊢ \prod_{𝑡} (F) \in PConn \leftrightarrow (\prod_{𝑡} (F) \in Top \land \forall x \in ⋃ \prod_{𝑡} (F) \forall y \in ⋃ \prod_{𝑡} (F) \exists f \in (II Cn \prod_{𝑡} (F)) (f (0) = x \land f (1) = y))$
134	6 131 133	sylanbrc	$⊢ (A \in V \land F : A ⟶ PConn) \to \prod_{𝑡} (F) \in PConn$

Metamath Proof Explorer

Theorem ptpconn

Proof