Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) → ( ∏t ‘ 𝐹 ) ∈ PConn )

Proof

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