| Step | Hyp | Ref
| Expression |
| 1 | | pconntop 35230 |
. . . . 5
⊢ (𝑥 ∈ PConn → 𝑥 ∈ Top) |
| 2 | 1 | ssriv 3987 |
. . . 4
⊢ PConn
⊆ Top |
| 3 | | fss 6752 |
. . . 4
⊢ ((𝐹:𝐴⟶PConn ∧ PConn ⊆ Top)
→ 𝐹:𝐴⟶Top) |
| 4 | 2, 3 | mpan2 691 |
. . 3
⊢ (𝐹:𝐴⟶PConn → 𝐹:𝐴⟶Top) |
| 5 | | pttop 23590 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) →
(∏t‘𝐹) ∈ Top) |
| 6 | 4, 5 | sylan2 593 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) →
(∏t‘𝐹) ∈ Top) |
| 7 | | fvi 6985 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ( I ‘𝐴) = 𝐴) |
| 9 | 8 | eleq2d 2827 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (𝑡 ∈ ( I ‘𝐴) ↔ 𝑡 ∈ 𝐴)) |
| 10 | 9 | biimpa 476 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑡 ∈ ( I ‘𝐴)) → 𝑡 ∈ 𝐴) |
| 11 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝐹:𝐴⟶PConn) |
| 12 | 11 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑡 ∈ 𝐴) → (𝐹‘𝑡) ∈ PConn) |
| 13 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑥 ∈ ∪
(∏t‘𝐹)) |
| 14 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(∏t‘𝐹) = (∏t‘𝐹) |
| 15 | 14 | ptuni 23602 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑡 ∈
𝐴 ∪ (𝐹‘𝑡) = ∪
(∏t‘𝐹)) |
| 16 | 4, 15 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) → X𝑡 ∈
𝐴 ∪ (𝐹‘𝑡) = ∪
(∏t‘𝐹)) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → X𝑡 ∈ 𝐴 ∪ (𝐹‘𝑡) = ∪
(∏t‘𝐹)) |
| 18 | 13, 17 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑥 ∈ X𝑡 ∈ 𝐴 ∪ (𝐹‘𝑡)) |
| 19 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 20 | 19 | elixp 8944 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ X𝑡 ∈
𝐴 ∪ (𝐹‘𝑡) ↔ (𝑥 Fn 𝐴 ∧ ∀𝑡 ∈ 𝐴 (𝑥‘𝑡) ∈ ∪ (𝐹‘𝑡))) |
| 21 | 18, 20 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (𝑥 Fn 𝐴 ∧ ∀𝑡 ∈ 𝐴 (𝑥‘𝑡) ∈ ∪ (𝐹‘𝑡))) |
| 22 | 21 | simprd 495 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ∀𝑡 ∈ 𝐴 (𝑥‘𝑡) ∈ ∪ (𝐹‘𝑡)) |
| 23 | 22 | r19.21bi 3251 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑡 ∈ 𝐴) → (𝑥‘𝑡) ∈ ∪ (𝐹‘𝑡)) |
| 24 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑦 ∈ ∪
(∏t‘𝐹)) |
| 25 | 24, 17 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑦 ∈ X𝑡 ∈ 𝐴 ∪ (𝐹‘𝑡)) |
| 26 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
| 27 | 26 | elixp 8944 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ X𝑡 ∈
𝐴 ∪ (𝐹‘𝑡) ↔ (𝑦 Fn 𝐴 ∧ ∀𝑡 ∈ 𝐴 (𝑦‘𝑡) ∈ ∪ (𝐹‘𝑡))) |
| 28 | 25, 27 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → (𝑦 Fn 𝐴 ∧ ∀𝑡 ∈ 𝐴 (𝑦‘𝑡) ∈ ∪ (𝐹‘𝑡))) |
| 29 | 28 | simprd 495 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ∀𝑡 ∈ 𝐴 (𝑦‘𝑡) ∈ ∪ (𝐹‘𝑡)) |
| 30 | 29 | r19.21bi 3251 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑡 ∈ 𝐴) → (𝑦‘𝑡) ∈ ∪ (𝐹‘𝑡)) |
| 31 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ (𝐹‘𝑡) = ∪ (𝐹‘𝑡) |
| 32 | 31 | pconncn 35229 |
. . . . . . . . 9
⊢ (((𝐹‘𝑡) ∈ PConn ∧ (𝑥‘𝑡) ∈ ∪ (𝐹‘𝑡) ∧ (𝑦‘𝑡) ∈ ∪ (𝐹‘𝑡)) → ∃𝑓 ∈ (II Cn (𝐹‘𝑡))((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡))) |
| 33 | 12, 23, 30, 32 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑡 ∈ 𝐴) → ∃𝑓 ∈ (II Cn (𝐹‘𝑡))((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡))) |
| 34 | | df-rex 3071 |
. . . . . . . 8
⊢
(∃𝑓 ∈ (II
Cn (𝐹‘𝑡))((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡)) ↔ ∃𝑓(𝑓 ∈ (II Cn (𝐹‘𝑡)) ∧ ((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡)))) |
| 35 | 33, 34 | sylib 218 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑡 ∈ 𝐴) → ∃𝑓(𝑓 ∈ (II Cn (𝐹‘𝑡)) ∧ ((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡)))) |
| 36 | 10, 35 | syldan 591 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ 𝑡 ∈ ( I ‘𝐴)) → ∃𝑓(𝑓 ∈ (II Cn (𝐹‘𝑡)) ∧ ((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡)))) |
| 37 | 36 | ralrimiva 3146 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ∀𝑡 ∈ ( I ‘𝐴)∃𝑓(𝑓 ∈ (II Cn (𝐹‘𝑡)) ∧ ((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡)))) |
| 38 | | fvex 6919 |
. . . . . 6
⊢ ( I
‘𝐴) ∈
V |
| 39 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑓 = (𝑔‘𝑡) → (𝑓 ∈ (II Cn (𝐹‘𝑡)) ↔ (𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)))) |
| 40 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔‘𝑡) → (𝑓‘0) = ((𝑔‘𝑡)‘0)) |
| 41 | 40 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑓 = (𝑔‘𝑡) → ((𝑓‘0) = (𝑥‘𝑡) ↔ ((𝑔‘𝑡)‘0) = (𝑥‘𝑡))) |
| 42 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔‘𝑡) → (𝑓‘1) = ((𝑔‘𝑡)‘1)) |
| 43 | 42 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑓 = (𝑔‘𝑡) → ((𝑓‘1) = (𝑦‘𝑡) ↔ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))) |
| 44 | 41, 43 | anbi12d 632 |
. . . . . . 7
⊢ (𝑓 = (𝑔‘𝑡) → (((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡)) ↔ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡)))) |
| 45 | 39, 44 | anbi12d 632 |
. . . . . 6
⊢ (𝑓 = (𝑔‘𝑡) → ((𝑓 ∈ (II Cn (𝐹‘𝑡)) ∧ ((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡))) ↔ ((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) |
| 46 | 38, 45 | ac6s2 10526 |
. . . . 5
⊢
(∀𝑡 ∈ (
I ‘𝐴)∃𝑓(𝑓 ∈ (II Cn (𝐹‘𝑡)) ∧ ((𝑓‘0) = (𝑥‘𝑡) ∧ (𝑓‘1) = (𝑦‘𝑡))) → ∃𝑔(𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) |
| 47 | 37, 46 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ∃𝑔(𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) |
| 48 | | iitopon 24905 |
. . . . . . 7
⊢ II ∈
(TopOn‘(0[,]1)) |
| 49 | 48 | a1i 11 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → II ∈
(TopOn‘(0[,]1))) |
| 50 | | simplll 775 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → 𝐴 ∈ 𝑉) |
| 51 | 11 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → 𝐹:𝐴⟶PConn) |
| 52 | 51, 4 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → 𝐹:𝐴⟶Top) |
| 53 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → ( I ‘𝐴) = 𝐴) |
| 54 | 53 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → (𝑖 ∈ ( I ‘𝐴) ↔ 𝑖 ∈ 𝐴)) |
| 55 | 54 | biimpar 477 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ ( I ‘𝐴)) |
| 56 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡)))) |
| 57 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑖 → (𝑔‘𝑡) = (𝑔‘𝑖)) |
| 58 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑖 → (𝐹‘𝑡) = (𝐹‘𝑖)) |
| 59 | 58 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑖 → (II Cn (𝐹‘𝑡)) = (II Cn (𝐹‘𝑖))) |
| 60 | 57, 59 | eleq12d 2835 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑖 → ((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ↔ (𝑔‘𝑖) ∈ (II Cn (𝐹‘𝑖)))) |
| 61 | 57 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑖 → ((𝑔‘𝑡)‘0) = ((𝑔‘𝑖)‘0)) |
| 62 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑖 → (𝑥‘𝑡) = (𝑥‘𝑖)) |
| 63 | 61, 62 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑖 → (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ↔ ((𝑔‘𝑖)‘0) = (𝑥‘𝑖))) |
| 64 | 57 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑖 → ((𝑔‘𝑡)‘1) = ((𝑔‘𝑖)‘1)) |
| 65 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑖 → (𝑦‘𝑡) = (𝑦‘𝑖)) |
| 66 | 64, 65 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑖 → (((𝑔‘𝑡)‘1) = (𝑦‘𝑡) ↔ ((𝑔‘𝑖)‘1) = (𝑦‘𝑖))) |
| 67 | 63, 66 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑖 → ((((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡)) ↔ (((𝑔‘𝑖)‘0) = (𝑥‘𝑖) ∧ ((𝑔‘𝑖)‘1) = (𝑦‘𝑖)))) |
| 68 | 60, 67 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑖 → (((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))) ↔ ((𝑔‘𝑖) ∈ (II Cn (𝐹‘𝑖)) ∧ (((𝑔‘𝑖)‘0) = (𝑥‘𝑖) ∧ ((𝑔‘𝑖)‘1) = (𝑦‘𝑖))))) |
| 69 | 68 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑡 ∈ (
I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))) ∧ 𝑖 ∈ ( I ‘𝐴)) → ((𝑔‘𝑖) ∈ (II Cn (𝐹‘𝑖)) ∧ (((𝑔‘𝑖)‘0) = (𝑥‘𝑖) ∧ ((𝑔‘𝑖)‘1) = (𝑦‘𝑖)))) |
| 70 | 56, 69 | sylan 580 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ ( I ‘𝐴)) → ((𝑔‘𝑖) ∈ (II Cn (𝐹‘𝑖)) ∧ (((𝑔‘𝑖)‘0) = (𝑥‘𝑖) ∧ ((𝑔‘𝑖)‘1) = (𝑦‘𝑖)))) |
| 71 | 55, 70 | syldan 591 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → ((𝑔‘𝑖) ∈ (II Cn (𝐹‘𝑖)) ∧ (((𝑔‘𝑖)‘0) = (𝑥‘𝑖) ∧ ((𝑔‘𝑖)‘1) = (𝑦‘𝑖)))) |
| 72 | 71 | simpld 494 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → (𝑔‘𝑖) ∈ (II Cn (𝐹‘𝑖))) |
| 73 | | iiuni 24907 |
. . . . . . . . . 10
⊢ (0[,]1) =
∪ II |
| 74 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ (𝐹‘𝑖) = ∪ (𝐹‘𝑖) |
| 75 | 73, 74 | cnf 23254 |
. . . . . . . . 9
⊢ ((𝑔‘𝑖) ∈ (II Cn (𝐹‘𝑖)) → (𝑔‘𝑖):(0[,]1)⟶∪
(𝐹‘𝑖)) |
| 76 | 72, 75 | syl 17 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → (𝑔‘𝑖):(0[,]1)⟶∪
(𝐹‘𝑖)) |
| 77 | 76 | feqmptd 6977 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → (𝑔‘𝑖) = (𝑧 ∈ (0[,]1) ↦ ((𝑔‘𝑖)‘𝑧))) |
| 78 | 77, 72 | eqeltrrd 2842 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → (𝑧 ∈ (0[,]1) ↦ ((𝑔‘𝑖)‘𝑧)) ∈ (II Cn (𝐹‘𝑖))) |
| 79 | 14, 49, 50, 52, 78 | ptcn 23635 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) ∈ (II Cn
(∏t‘𝐹))) |
| 80 | 71 | simprd 495 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → (((𝑔‘𝑖)‘0) = (𝑥‘𝑖) ∧ ((𝑔‘𝑖)‘1) = (𝑦‘𝑖))) |
| 81 | 80 | simpld 494 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → ((𝑔‘𝑖)‘0) = (𝑥‘𝑖)) |
| 82 | 81 | mpteq2dva 5242 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘0)) = (𝑖 ∈ 𝐴 ↦ (𝑥‘𝑖))) |
| 83 | | 0elunit 13509 |
. . . . . . 7
⊢ 0 ∈
(0[,]1) |
| 84 | | mptexg 7241 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘0)) ∈ V) |
| 85 | 50, 84 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘0)) ∈ V) |
| 86 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑧 = 0 → ((𝑔‘𝑖)‘𝑧) = ((𝑔‘𝑖)‘0)) |
| 87 | 86 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑧 = 0 → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)) = (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘0))) |
| 88 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) = (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) |
| 89 | 87, 88 | fvmptg 7014 |
. . . . . . 7
⊢ ((0
∈ (0[,]1) ∧ (𝑖
∈ 𝐴 ↦ ((𝑔‘𝑖)‘0)) ∈ V) → ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘0) = (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘0))) |
| 90 | 83, 85, 89 | sylancr 587 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘0) = (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘0))) |
| 91 | 21 | simpld 494 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑥 Fn 𝐴) |
| 92 | 91 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → 𝑥 Fn 𝐴) |
| 93 | | dffn5 6967 |
. . . . . . 7
⊢ (𝑥 Fn 𝐴 ↔ 𝑥 = (𝑖 ∈ 𝐴 ↦ (𝑥‘𝑖))) |
| 94 | 92, 93 | sylib 218 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → 𝑥 = (𝑖 ∈ 𝐴 ↦ (𝑥‘𝑖))) |
| 95 | 82, 90, 94 | 3eqtr4d 2787 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘0) = 𝑥) |
| 96 | 80 | simprd 495 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) ∧ 𝑖 ∈ 𝐴) → ((𝑔‘𝑖)‘1) = (𝑦‘𝑖)) |
| 97 | 96 | mpteq2dva 5242 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘1)) = (𝑖 ∈ 𝐴 ↦ (𝑦‘𝑖))) |
| 98 | | 1elunit 13510 |
. . . . . . 7
⊢ 1 ∈
(0[,]1) |
| 99 | | mptexg 7241 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘1)) ∈ V) |
| 100 | 50, 99 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘1)) ∈ V) |
| 101 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑧 = 1 → ((𝑔‘𝑖)‘𝑧) = ((𝑔‘𝑖)‘1)) |
| 102 | 101 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑧 = 1 → (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)) = (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘1))) |
| 103 | 102, 88 | fvmptg 7014 |
. . . . . . 7
⊢ ((1
∈ (0[,]1) ∧ (𝑖
∈ 𝐴 ↦ ((𝑔‘𝑖)‘1)) ∈ V) → ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘1) = (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘1))) |
| 104 | 98, 100, 103 | sylancr 587 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘1) = (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘1))) |
| 105 | 28 | simpld 494 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → 𝑦 Fn 𝐴) |
| 106 | 105 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → 𝑦 Fn 𝐴) |
| 107 | | dffn5 6967 |
. . . . . . 7
⊢ (𝑦 Fn 𝐴 ↔ 𝑦 = (𝑖 ∈ 𝐴 ↦ (𝑦‘𝑖))) |
| 108 | 106, 107 | sylib 218 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → 𝑦 = (𝑖 ∈ 𝐴 ↦ (𝑦‘𝑖))) |
| 109 | 97, 104, 108 | 3eqtr4d 2787 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘1) = 𝑦) |
| 110 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) → (𝑓‘0) = ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘0)) |
| 111 | 110 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) → ((𝑓‘0) = 𝑥 ↔ ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘0) = 𝑥)) |
| 112 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) → (𝑓‘1) = ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘1)) |
| 113 | 112 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) → ((𝑓‘1) = 𝑦 ↔ ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘1) = 𝑦)) |
| 114 | 111, 113 | anbi12d 632 |
. . . . . 6
⊢ (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ (((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘0) = 𝑥 ∧ ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘1) = 𝑦))) |
| 115 | 114 | rspcev 3622 |
. . . . 5
⊢ (((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧))) ∈ (II Cn
(∏t‘𝐹)) ∧ (((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘0) = 𝑥 ∧ ((𝑧 ∈ (0[,]1) ↦ (𝑖 ∈ 𝐴 ↦ ((𝑔‘𝑖)‘𝑧)))‘1) = 𝑦)) → ∃𝑓 ∈ (II Cn
(∏t‘𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 116 | 79, 95, 109, 115 | syl12anc 837 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔‘𝑡) ∈ (II Cn (𝐹‘𝑡)) ∧ (((𝑔‘𝑡)‘0) = (𝑥‘𝑡) ∧ ((𝑔‘𝑡)‘1) = (𝑦‘𝑡))))) → ∃𝑓 ∈ (II Cn
(∏t‘𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 117 | 47, 116 | exlimddv 1935 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) ∧ (𝑥 ∈ ∪
(∏t‘𝐹) ∧ 𝑦 ∈ ∪
(∏t‘𝐹))) → ∃𝑓 ∈ (II Cn
(∏t‘𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 118 | 117 | ralrimivva 3202 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) → ∀𝑥 ∈ ∪ (∏t‘𝐹)∀𝑦 ∈ ∪
(∏t‘𝐹)∃𝑓 ∈ (II Cn
(∏t‘𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 119 | | eqid 2737 |
. . 3
⊢ ∪ (∏t‘𝐹) = ∪
(∏t‘𝐹) |
| 120 | 119 | ispconn 35228 |
. 2
⊢
((∏t‘𝐹) ∈ PConn ↔
((∏t‘𝐹) ∈ Top ∧ ∀𝑥 ∈ ∪ (∏t‘𝐹)∀𝑦 ∈ ∪
(∏t‘𝐹)∃𝑓 ∈ (II Cn
(∏t‘𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) |
| 121 | 6, 118, 120 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) →
(∏t‘𝐹) ∈ PConn) |