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)

		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		fvi	$⊢ A \in V \to I (A) = A$
8	7	ad2antrr	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to I (A) = A$
9	8	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)$
10	9	biimpa	$⊢ (((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land t \in I (A)) \to t \in A$
11		simplr	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to F : A ⟶ PConn$
12	11	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$
13		simprl	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x \in ⋃ \prod_{𝑡} (F)$
14		eqid	$⊢ \prod_{𝑡} (F) = \prod_{𝑡} (F)$
15	14	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{t \in A}{⨉} ⋃ F (t) = ⋃ \prod_{𝑡} (F)$
16	4 15	sylan2	$⊢ (A \in V \land F : A ⟶ PConn) \to \underset{t \in A}{⨉} ⋃ F (t) = ⋃ \prod_{𝑡} (F)$
17	16	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)$
18	13 17	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)$
19		vex	$⊢ x \in V$
20	19	elixp	$⊢ x \in \underset{t \in A}{⨉} ⋃ F (t) \leftrightarrow (x Fn A \land \forall t \in A x (t) \in ⋃ F (t))$
21	18 20	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))$
22	21	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)$
23	22	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)$
24		simprr	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y \in ⋃ \prod_{𝑡} (F)$
25	24 17	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)$
26		vex	$⊢ y \in V$
27	26	elixp	$⊢ y \in \underset{t \in A}{⨉} ⋃ F (t) \leftrightarrow (y Fn A \land \forall t \in A y (t) \in ⋃ F (t))$
28	25 27	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))$
29	28	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)$
30	29	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)$
31		eqid	$⊢ ⋃ F (t) = ⋃ F (t)$
32	31	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))$
33	12 23 30 32	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))$
34		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)))$
35	33 34	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)))$
36	10 35	syldan	$⊢ (((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)))$
37	36	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)))$
38		fvex	$⊢ I (A) \in V$
39		eleq1	$⊢ f = g (t) \to (f \in (II Cn F (t)) \leftrightarrow g (t) \in (II Cn F (t)))$
40		fveq1	$⊢ f = g (t) \to f (0) = g (t) (0)$
41	40	eqeq1d	$⊢ f = g (t) \to (f (0) = x (t) \leftrightarrow g (t) (0) = x (t))$
42		fveq1	$⊢ f = g (t) \to f (1) = g (t) (1)$
43	42	eqeq1d	$⊢ f = g (t) \to (f (1) = y (t) \leftrightarrow g (t) (1) = y (t))$
44	41 43	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)))$
45	39 44	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))))$
46	38 45	ac6s2	$⊢ \forall t \in I (A) \exists f (f \in (II Cn F (t)) \land (f (0) = x (t) \land f (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))))$
47	37 46	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))))$
48		iitopon	$⊢ II \in TopOn ([0, 1])$
49	48	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])$
50		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$
51	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 F : A ⟶ PConn$
52	51 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$
53	8	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$
54	53	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)$
55	54	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)$
56		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)))$
57		fveq2	$⊢ t = i \to g (t) = g (i)$
58		fveq2	$⊢ t = i \to F (t) = F (i)$
59	58	oveq2d	$⊢ t = i \to II Cn F (t) = II Cn F (i)$
60	57 59	eleq12d	$⊢ t = i \to (g (t) \in (II Cn F (t)) \leftrightarrow g (i) \in (II Cn F (i)))$
61	57	fveq1d	$⊢ t = i \to g (t) (0) = g (i) (0)$
62		fveq2	$⊢ t = i \to x (t) = x (i)$
63	61 62	eqeq12d	$⊢ t = i \to (g (t) (0) = x (t) \leftrightarrow g (i) (0) = x (i))$
64	57	fveq1d	$⊢ t = i \to g (t) (1) = g (i) (1)$
65		fveq2	$⊢ t = i \to y (t) = y (i)$
66	64 65	eqeq12d	$⊢ t = i \to (g (t) (1) = y (t) \leftrightarrow g (i) (1) = y (i))$
67	63 66	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)))$
68	60 67	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))))$
69	68	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)))$
70	56 69	sylan	$⊢ ((((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 I (A)) \to (g (i) \in (II Cn F (i)) \land (g (i) (0) = x (i) \land g (i) (1) = y (i)))$
71	55 70	syldan	$⊢ ((((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)))$
72	71	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))$
73		iiuni	$⊢ [0, 1] = ⋃ II$
74		eqid	$⊢ ⋃ F (i) = ⋃ F (i)$
75	73 74	cnf	$⊢ g (i) \in (II Cn F (i)) \to g (i) : [0, 1] ⟶ ⋃ F (i)$
76	72 75	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)$
77	76	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))$
78	77 72	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))$
79	14 49 50 52 78	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))$
80	71	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))$
81	80	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)$
82	81	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))$
83		0elunit	$⊢ 0 \in [0, 1]$
84		mptexg	$⊢ A \in V \to (i \in A ⟼ g (i) (0)) \in V$
85	50 84	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 (i \in A ⟼ g (i) (0)) \in V$
86		fveq2	$⊢ z = 0 \to g (i) (z) = g (i) (0)$
87	86	mpteq2dv	$⊢ z = 0 \to (i \in A ⟼ g (i) (z)) = (i \in A ⟼ g (i) (0))$
88		eqid	$⊢ (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z))) = (z \in [0, 1] ⟼ (i \in A ⟼ g (i) (z)))$
89	87 88	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))$
90	83 85 89	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))$
91	21	simpld	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x Fn A$
92	91	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$
93		dffn5	$⊢ x Fn A \leftrightarrow x = (i \in A ⟼ x (i))$
94	92 93	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))$
95	82 90 94	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$
96	80	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)$
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) (1)) = (i \in A ⟼ y (i))$
98		1elunit	$⊢ 1 \in [0, 1]$
99		mptexg	$⊢ A \in V \to (i \in A ⟼ g (i) (1)) \in V$
100	50 99	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 (i \in A ⟼ g (i) (1)) \in V$
101		fveq2	$⊢ z = 1 \to g (i) (z) = g (i) (1)$
102	101	mpteq2dv	$⊢ z = 1 \to (i \in A ⟼ g (i) (z)) = (i \in A ⟼ g (i) (1))$
103	102 88	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))$
104	98 100 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))) (1) = (i \in A ⟼ g (i) (1))$
105	28	simpld	$⊢ ((A \in V \land F : A ⟶ PConn) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y 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 y Fn A$
107		dffn5	$⊢ y Fn A \leftrightarrow y = (i \in A ⟼ y (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 y = (i \in A ⟼ y (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))) (1) = y$
110		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)$
111	110	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)$
112		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)$
113	112	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)$
114	111 113	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))$
115	114	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)$
116	79 95 109 115	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)$
117	47 116	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)$
118	117	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)$
119		eqid	$⊢ ⋃ \prod_{𝑡} (F) = ⋃ \prod_{𝑡} (F)$
120	119	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))$
121	6 118 120	sylanbrc	$⊢ (A \in V \land F : A ⟶ PConn) \to \prod_{𝑡} (F) \in PConn$

Metamath Proof Explorer

Theorem ptpconn

Proof