| 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 |
|
fvi |
⊢ ( 𝐴 ∈ 𝑉 → ( I ‘ 𝐴 ) = 𝐴 ) |
| 8 |
7
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( I ‘ 𝐴 ) = 𝐴 ) |
| 9 |
8
|
eleq2d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑡 ∈ ( I ‘ 𝐴 ) ↔ 𝑡 ∈ 𝐴 ) ) |
| 10 |
9
|
biimpa |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑡 ∈ ( I ‘ 𝐴 ) ) → 𝑡 ∈ 𝐴 ) |
| 11 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝐹 : 𝐴 ⟶ PConn ) |
| 12 |
11
|
ffvelcdmda |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ PConn ) |
| 13 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ) |
| 14 |
|
eqid |
⊢ ( ∏t ‘ 𝐹 ) = ( ∏t ‘ 𝐹 ) |
| 15 |
14
|
ptuni |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑡 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑡 ) = ∪ ( ∏t ‘ 𝐹 ) ) |
| 16 |
4 15
|
sylan2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) → X 𝑡 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑡 ) = ∪ ( ∏t ‘ 𝐹 ) ) |
| 17 |
16
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → X 𝑡 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑡 ) = ∪ ( ∏t ‘ 𝐹 ) ) |
| 18 |
13 17
|
eleqtrrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 ∈ X 𝑡 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑡 ) ) |
| 19 |
|
vex |
⊢ 𝑥 ∈ V |
| 20 |
19
|
elixp |
⊢ ( 𝑥 ∈ X 𝑡 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑡 ) ↔ ( 𝑥 Fn 𝐴 ∧ ∀ 𝑡 ∈ 𝐴 ( 𝑥 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) ) |
| 21 |
18 20
|
sylib |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑥 Fn 𝐴 ∧ ∀ 𝑡 ∈ 𝐴 ( 𝑥 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) ) |
| 22 |
21
|
simprd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∀ 𝑡 ∈ 𝐴 ( 𝑥 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) |
| 23 |
22
|
r19.21bi |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑡 ∈ 𝐴 ) → ( 𝑥 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) |
| 24 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) |
| 25 |
24 17
|
eleqtrrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑦 ∈ X 𝑡 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑡 ) ) |
| 26 |
|
vex |
⊢ 𝑦 ∈ V |
| 27 |
26
|
elixp |
⊢ ( 𝑦 ∈ X 𝑡 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑡 ) ↔ ( 𝑦 Fn 𝐴 ∧ ∀ 𝑡 ∈ 𝐴 ( 𝑦 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) ) |
| 28 |
25 27
|
sylib |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ( 𝑦 Fn 𝐴 ∧ ∀ 𝑡 ∈ 𝐴 ( 𝑦 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) ) |
| 29 |
28
|
simprd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∀ 𝑡 ∈ 𝐴 ( 𝑦 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) |
| 30 |
29
|
r19.21bi |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑡 ∈ 𝐴 ) → ( 𝑦 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) |
| 31 |
|
eqid |
⊢ ∪ ( 𝐹 ‘ 𝑡 ) = ∪ ( 𝐹 ‘ 𝑡 ) |
| 32 |
31
|
pconncn |
⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ PConn ∧ ( 𝑥 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ∈ ∪ ( 𝐹 ‘ 𝑡 ) ) → ∃ 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) |
| 33 |
12 23 30 32
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑡 ∈ 𝐴 ) → ∃ 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) |
| 34 |
|
df-rex |
⊢ ( ∃ 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) |
| 35 |
33 34
|
sylib |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑡 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) |
| 36 |
10 35
|
syldan |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ 𝑡 ∈ ( I ‘ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) |
| 37 |
36
|
ralrimiva |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ∃ 𝑓 ( 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) |
| 38 |
|
fvex |
⊢ ( I ‘ 𝐴 ) ∈ V |
| 39 |
|
eleq1 |
⊢ ( 𝑓 = ( 𝑔 ‘ 𝑡 ) → ( 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ↔ ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ) ) |
| 40 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑔 ‘ 𝑡 ) → ( 𝑓 ‘ 0 ) = ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) ) |
| 41 |
40
|
eqeq1d |
⊢ ( 𝑓 = ( 𝑔 ‘ 𝑡 ) → ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ↔ ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ) ) |
| 42 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑔 ‘ 𝑡 ) → ( 𝑓 ‘ 1 ) = ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) ) |
| 43 |
42
|
eqeq1d |
⊢ ( 𝑓 = ( 𝑔 ‘ 𝑡 ) → ( ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ↔ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) |
| 44 |
41 43
|
anbi12d |
⊢ ( 𝑓 = ( 𝑔 ‘ 𝑡 ) → ( ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ↔ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) |
| 45 |
39 44
|
anbi12d |
⊢ ( 𝑓 = ( 𝑔 ‘ 𝑡 ) → ( ( 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ↔ ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) |
| 46 |
38 45
|
ac6s2 |
⊢ ( ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ∃ 𝑓 ( 𝑓 ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( 𝑓 ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) |
| 47 |
37 46
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) |
| 48 |
|
iitopon |
⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) |
| 49 |
48
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ) |
| 50 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → 𝐴 ∈ 𝑉 ) |
| 51 |
11
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → 𝐹 : 𝐴 ⟶ PConn ) |
| 52 |
51 4
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → 𝐹 : 𝐴 ⟶ Top ) |
| 53 |
8
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( I ‘ 𝐴 ) = 𝐴 ) |
| 54 |
53
|
eleq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( 𝑖 ∈ ( I ‘ 𝐴 ) ↔ 𝑖 ∈ 𝐴 ) ) |
| 55 |
54
|
biimpar |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → 𝑖 ∈ ( I ‘ 𝐴 ) ) |
| 56 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) |
| 57 |
|
fveq2 |
⊢ ( 𝑡 = 𝑖 → ( 𝑔 ‘ 𝑡 ) = ( 𝑔 ‘ 𝑖 ) ) |
| 58 |
|
fveq2 |
⊢ ( 𝑡 = 𝑖 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑖 ) ) |
| 59 |
58
|
oveq2d |
⊢ ( 𝑡 = 𝑖 → ( II Cn ( 𝐹 ‘ 𝑡 ) ) = ( II Cn ( 𝐹 ‘ 𝑖 ) ) ) |
| 60 |
57 59
|
eleq12d |
⊢ ( 𝑡 = 𝑖 → ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ↔ ( 𝑔 ‘ 𝑖 ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) ) ) |
| 61 |
57
|
fveq1d |
⊢ ( 𝑡 = 𝑖 → ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) |
| 62 |
|
fveq2 |
⊢ ( 𝑡 = 𝑖 → ( 𝑥 ‘ 𝑡 ) = ( 𝑥 ‘ 𝑖 ) ) |
| 63 |
61 62
|
eqeq12d |
⊢ ( 𝑡 = 𝑖 → ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ↔ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ) ) |
| 64 |
57
|
fveq1d |
⊢ ( 𝑡 = 𝑖 → ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) |
| 65 |
|
fveq2 |
⊢ ( 𝑡 = 𝑖 → ( 𝑦 ‘ 𝑡 ) = ( 𝑦 ‘ 𝑖 ) ) |
| 66 |
64 65
|
eqeq12d |
⊢ ( 𝑡 = 𝑖 → ( ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ↔ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) ) |
| 67 |
63 66
|
anbi12d |
⊢ ( 𝑡 = 𝑖 → ( ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ↔ ( ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ∧ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 68 |
60 67
|
anbi12d |
⊢ ( 𝑡 = 𝑖 → ( ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ↔ ( ( 𝑔 ‘ 𝑖 ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) ∧ ( ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ∧ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 69 |
68
|
rspccva |
⊢ ( ( ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ∧ 𝑖 ∈ ( I ‘ 𝐴 ) ) → ( ( 𝑔 ‘ 𝑖 ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) ∧ ( ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ∧ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 70 |
56 69
|
sylan |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ ( I ‘ 𝐴 ) ) → ( ( 𝑔 ‘ 𝑖 ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) ∧ ( ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ∧ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 71 |
55 70
|
syldan |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑔 ‘ 𝑖 ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) ∧ ( ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ∧ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 72 |
71
|
simpld |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑖 ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) ) |
| 73 |
|
iiuni |
⊢ ( 0 [,] 1 ) = ∪ II |
| 74 |
|
eqid |
⊢ ∪ ( 𝐹 ‘ 𝑖 ) = ∪ ( 𝐹 ‘ 𝑖 ) |
| 75 |
73 74
|
cnf |
⊢ ( ( 𝑔 ‘ 𝑖 ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) → ( 𝑔 ‘ 𝑖 ) : ( 0 [,] 1 ) ⟶ ∪ ( 𝐹 ‘ 𝑖 ) ) |
| 76 |
72 75
|
syl |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑖 ) : ( 0 [,] 1 ) ⟶ ∪ ( 𝐹 ‘ 𝑖 ) ) |
| 77 |
76
|
feqmptd |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) |
| 78 |
77 72
|
eqeltrrd |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ∈ ( II Cn ( 𝐹 ‘ 𝑖 ) ) ) |
| 79 |
14 49 50 52 78
|
ptcn |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ∈ ( II Cn ( ∏t ‘ 𝐹 ) ) ) |
| 80 |
71
|
simprd |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ∧ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) ) |
| 81 |
80
|
simpld |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) = ( 𝑥 ‘ 𝑖 ) ) |
| 82 |
81
|
mpteq2dva |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) = ( 𝑖 ∈ 𝐴 ↦ ( 𝑥 ‘ 𝑖 ) ) ) |
| 83 |
|
0elunit |
⊢ 0 ∈ ( 0 [,] 1 ) |
| 84 |
|
mptexg |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) ∈ V ) |
| 85 |
50 84
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) ∈ V ) |
| 86 |
|
fveq2 |
⊢ ( 𝑧 = 0 → ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) = ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) |
| 87 |
86
|
mpteq2dv |
⊢ ( 𝑧 = 0 → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) = ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) ) |
| 88 |
|
eqid |
⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) |
| 89 |
87 88
|
fvmptg |
⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) ∈ V ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 0 ) = ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) ) |
| 90 |
83 85 89
|
sylancr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 0 ) = ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 0 ) ) ) |
| 91 |
21
|
simpld |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → 𝑥 Fn 𝐴 ) |
| 92 |
91
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → 𝑥 Fn 𝐴 ) |
| 93 |
|
dffn5 |
⊢ ( 𝑥 Fn 𝐴 ↔ 𝑥 = ( 𝑖 ∈ 𝐴 ↦ ( 𝑥 ‘ 𝑖 ) ) ) |
| 94 |
92 93
|
sylib |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → 𝑥 = ( 𝑖 ∈ 𝐴 ↦ ( 𝑥 ‘ 𝑖 ) ) ) |
| 95 |
82 90 94
|
3eqtr4d |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 0 ) = 𝑥 ) |
| 96 |
80
|
simprd |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) = ( 𝑦 ‘ 𝑖 ) ) |
| 97 |
96
|
mpteq2dva |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) = ( 𝑖 ∈ 𝐴 ↦ ( 𝑦 ‘ 𝑖 ) ) ) |
| 98 |
|
1elunit |
⊢ 1 ∈ ( 0 [,] 1 ) |
| 99 |
|
mptexg |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) ∈ V ) |
| 100 |
50 99
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) ∈ V ) |
| 101 |
|
fveq2 |
⊢ ( 𝑧 = 1 → ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) = ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) |
| 102 |
101
|
mpteq2dv |
⊢ ( 𝑧 = 1 → ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) = ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) ) |
| 103 |
102 88
|
fvmptg |
⊢ ( ( 1 ∈ ( 0 [,] 1 ) ∧ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) ∈ V ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 1 ) = ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) ) |
| 104 |
98 100 103
|
sylancr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 1 ) = ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 1 ) ) ) |
| 105 |
28
|
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 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 1 ) = 𝑦 ) |
| 110 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) → ( 𝑓 ‘ 0 ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 0 ) ) |
| 111 |
110
|
eqeq1d |
⊢ ( 𝑓 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) → ( ( 𝑓 ‘ 0 ) = 𝑥 ↔ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 0 ) = 𝑥 ) ) |
| 112 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) → ( 𝑓 ‘ 1 ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 1 ) ) |
| 113 |
112
|
eqeq1d |
⊢ ( 𝑓 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) → ( ( 𝑓 ‘ 1 ) = 𝑦 ↔ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 1 ) = 𝑦 ) ) |
| 114 |
111 113
|
anbi12d |
⊢ ( 𝑓 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) → ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 0 ) = 𝑥 ∧ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 1 ) = 𝑦 ) ) ) |
| 115 |
114
|
rspcev |
⊢ ( ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ∈ ( II Cn ( ∏t ‘ 𝐹 ) ) ∧ ( ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 0 ) = 𝑥 ∧ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑖 ∈ 𝐴 ↦ ( ( 𝑔 ‘ 𝑖 ) ‘ 𝑧 ) ) ) ‘ 1 ) = 𝑦 ) ) → ∃ 𝑓 ∈ ( II Cn ( ∏t ‘ 𝐹 ) ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 116 |
79 95 109 115
|
syl12anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) ∧ ( 𝑔 Fn ( I ‘ 𝐴 ) ∧ ∀ 𝑡 ∈ ( I ‘ 𝐴 ) ( ( 𝑔 ‘ 𝑡 ) ∈ ( II Cn ( 𝐹 ‘ 𝑡 ) ) ∧ ( ( ( 𝑔 ‘ 𝑡 ) ‘ 0 ) = ( 𝑥 ‘ 𝑡 ) ∧ ( ( 𝑔 ‘ 𝑡 ) ‘ 1 ) = ( 𝑦 ‘ 𝑡 ) ) ) ) ) → ∃ 𝑓 ∈ ( II Cn ( ∏t ‘ 𝐹 ) ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 117 |
47 116
|
exlimddv |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) ∧ ( 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∧ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ) ) → ∃ 𝑓 ∈ ( II Cn ( ∏t ‘ 𝐹 ) ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 118 |
117
|
ralrimivva |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) → ∀ 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∀ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ∃ 𝑓 ∈ ( II Cn ( ∏t ‘ 𝐹 ) ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 119 |
|
eqid |
⊢ ∪ ( ∏t ‘ 𝐹 ) = ∪ ( ∏t ‘ 𝐹 ) |
| 120 |
119
|
ispconn |
⊢ ( ( ∏t ‘ 𝐹 ) ∈ PConn ↔ ( ( ∏t ‘ 𝐹 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( ∏t ‘ 𝐹 ) ∀ 𝑦 ∈ ∪ ( ∏t ‘ 𝐹 ) ∃ 𝑓 ∈ ( II Cn ( ∏t ‘ 𝐹 ) ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) ) |
| 121 |
6 118 120
|
sylanbrc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ PConn ) → ( ∏t ‘ 𝐹 ) ∈ PConn ) |