Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ptpconn Structured version   Visualization version   GIF version

Theorem ptpconn 31760
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.)
Assertion
Ref Expression
ptpconn ((𝐴𝑉𝐹:𝐴⟶PConn) → (∏t𝐹) ∈ PConn)

Proof of Theorem ptpconn
Dummy variables 𝑓 𝑥 𝑦 𝑔 𝑡 𝑧 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pconntop 31752 . . . . 5 (𝑥 ∈ PConn → 𝑥 ∈ Top)
21ssriv 3830 . . . 4 PConn ⊆ Top
3 fss 6290 . . . 4 ((𝐹:𝐴⟶PConn ∧ PConn ⊆ Top) → 𝐹:𝐴⟶Top)
42, 3mpan2 684 . . 3 (𝐹:𝐴⟶PConn → 𝐹:𝐴⟶Top)
5 pttop 21755 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) ∈ Top)
64, 5sylan2 588 . 2 ((𝐴𝑉𝐹:𝐴⟶PConn) → (∏t𝐹) ∈ Top)
7 fvi 6501 . . . . . . . . . 10 (𝐴𝑉 → ( I ‘𝐴) = 𝐴)
87ad2antrr 719 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ( I ‘𝐴) = 𝐴)
98eleq2d 2891 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑡 ∈ ( I ‘𝐴) ↔ 𝑡𝐴))
109biimpa 470 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑡 ∈ ( I ‘𝐴)) → 𝑡𝐴)
11 simplr 787 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝐹:𝐴⟶PConn)
1211ffvelrnda 6607 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑡𝐴) → (𝐹𝑡) ∈ PConn)
13 simprl 789 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥 (∏t𝐹))
14 eqid 2824 . . . . . . . . . . . . . . . 16 (∏t𝐹) = (∏t𝐹)
1514ptuni 21767 . . . . . . . . . . . . . . 15 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑡𝐴 (𝐹𝑡) = (∏t𝐹))
164, 15sylan2 588 . . . . . . . . . . . . . 14 ((𝐴𝑉𝐹:𝐴⟶PConn) → X𝑡𝐴 (𝐹𝑡) = (∏t𝐹))
1716adantr 474 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → X𝑡𝐴 (𝐹𝑡) = (∏t𝐹))
1813, 17eleqtrrd 2908 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥X𝑡𝐴 (𝐹𝑡))
19 vex 3416 . . . . . . . . . . . . 13 𝑥 ∈ V
2019elixp 8181 . . . . . . . . . . . 12 (𝑥X𝑡𝐴 (𝐹𝑡) ↔ (𝑥 Fn 𝐴 ∧ ∀𝑡𝐴 (𝑥𝑡) ∈ (𝐹𝑡)))
2118, 20sylib 210 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑥 Fn 𝐴 ∧ ∀𝑡𝐴 (𝑥𝑡) ∈ (𝐹𝑡)))
2221simprd 491 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∀𝑡𝐴 (𝑥𝑡) ∈ (𝐹𝑡))
2322r19.21bi 3140 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑡𝐴) → (𝑥𝑡) ∈ (𝐹𝑡))
24 simprr 791 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦 (∏t𝐹))
2524, 17eleqtrrd 2908 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦X𝑡𝐴 (𝐹𝑡))
26 vex 3416 . . . . . . . . . . . . 13 𝑦 ∈ V
2726elixp 8181 . . . . . . . . . . . 12 (𝑦X𝑡𝐴 (𝐹𝑡) ↔ (𝑦 Fn 𝐴 ∧ ∀𝑡𝐴 (𝑦𝑡) ∈ (𝐹𝑡)))
2825, 27sylib 210 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → (𝑦 Fn 𝐴 ∧ ∀𝑡𝐴 (𝑦𝑡) ∈ (𝐹𝑡)))
2928simprd 491 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∀𝑡𝐴 (𝑦𝑡) ∈ (𝐹𝑡))
3029r19.21bi 3140 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑡𝐴) → (𝑦𝑡) ∈ (𝐹𝑡))
31 eqid 2824 . . . . . . . . . 10 (𝐹𝑡) = (𝐹𝑡)
3231pconncn 31751 . . . . . . . . 9 (((𝐹𝑡) ∈ PConn ∧ (𝑥𝑡) ∈ (𝐹𝑡) ∧ (𝑦𝑡) ∈ (𝐹𝑡)) → ∃𝑓 ∈ (II Cn (𝐹𝑡))((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡)))
3312, 23, 30, 32syl3anc 1496 . . . . . . . 8 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑡𝐴) → ∃𝑓 ∈ (II Cn (𝐹𝑡))((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡)))
34 df-rex 3122 . . . . . . . 8 (∃𝑓 ∈ (II Cn (𝐹𝑡))((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡)) ↔ ∃𝑓(𝑓 ∈ (II Cn (𝐹𝑡)) ∧ ((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡))))
3533, 34sylib 210 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑡𝐴) → ∃𝑓(𝑓 ∈ (II Cn (𝐹𝑡)) ∧ ((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡))))
3610, 35syldan 587 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ 𝑡 ∈ ( I ‘𝐴)) → ∃𝑓(𝑓 ∈ (II Cn (𝐹𝑡)) ∧ ((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡))))
3736ralrimiva 3174 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∀𝑡 ∈ ( I ‘𝐴)∃𝑓(𝑓 ∈ (II Cn (𝐹𝑡)) ∧ ((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡))))
38 fvex 6445 . . . . . 6 ( I ‘𝐴) ∈ V
39 eleq1 2893 . . . . . . 7 (𝑓 = (𝑔𝑡) → (𝑓 ∈ (II Cn (𝐹𝑡)) ↔ (𝑔𝑡) ∈ (II Cn (𝐹𝑡))))
40 fveq1 6431 . . . . . . . . 9 (𝑓 = (𝑔𝑡) → (𝑓‘0) = ((𝑔𝑡)‘0))
4140eqeq1d 2826 . . . . . . . 8 (𝑓 = (𝑔𝑡) → ((𝑓‘0) = (𝑥𝑡) ↔ ((𝑔𝑡)‘0) = (𝑥𝑡)))
42 fveq1 6431 . . . . . . . . 9 (𝑓 = (𝑔𝑡) → (𝑓‘1) = ((𝑔𝑡)‘1))
4342eqeq1d 2826 . . . . . . . 8 (𝑓 = (𝑔𝑡) → ((𝑓‘1) = (𝑦𝑡) ↔ ((𝑔𝑡)‘1) = (𝑦𝑡)))
4441, 43anbi12d 626 . . . . . . 7 (𝑓 = (𝑔𝑡) → (((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡)) ↔ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))
4539, 44anbi12d 626 . . . . . 6 (𝑓 = (𝑔𝑡) → ((𝑓 ∈ (II Cn (𝐹𝑡)) ∧ ((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡))) ↔ ((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡)))))
4638, 45ac6s2 9622 . . . . 5 (∀𝑡 ∈ ( I ‘𝐴)∃𝑓(𝑓 ∈ (II Cn (𝐹𝑡)) ∧ ((𝑓‘0) = (𝑥𝑡) ∧ (𝑓‘1) = (𝑦𝑡))) → ∃𝑔(𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡)))))
4737, 46syl 17 . . . 4 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∃𝑔(𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡)))))
48 iitopon 23051 . . . . . . 7 II ∈ (TopOn‘(0[,]1))
4948a1i 11 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → II ∈ (TopOn‘(0[,]1)))
50 simplll 793 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → 𝐴𝑉)
5111adantr 474 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → 𝐹:𝐴⟶PConn)
5251, 4syl 17 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → 𝐹:𝐴⟶Top)
538adantr 474 . . . . . . . . . . . . 13 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → ( I ‘𝐴) = 𝐴)
5453eleq2d 2891 . . . . . . . . . . . 12 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → (𝑖 ∈ ( I ‘𝐴) ↔ 𝑖𝐴))
5554biimpar 471 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → 𝑖 ∈ ( I ‘𝐴))
56 simprr 791 . . . . . . . . . . . 12 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))
57 fveq2 6432 . . . . . . . . . . . . . . 15 (𝑡 = 𝑖 → (𝑔𝑡) = (𝑔𝑖))
58 fveq2 6432 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑖 → (𝐹𝑡) = (𝐹𝑖))
5958oveq2d 6920 . . . . . . . . . . . . . . 15 (𝑡 = 𝑖 → (II Cn (𝐹𝑡)) = (II Cn (𝐹𝑖)))
6057, 59eleq12d 2899 . . . . . . . . . . . . . 14 (𝑡 = 𝑖 → ((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ↔ (𝑔𝑖) ∈ (II Cn (𝐹𝑖))))
6157fveq1d 6434 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑖 → ((𝑔𝑡)‘0) = ((𝑔𝑖)‘0))
62 fveq2 6432 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑖 → (𝑥𝑡) = (𝑥𝑖))
6361, 62eqeq12d 2839 . . . . . . . . . . . . . . 15 (𝑡 = 𝑖 → (((𝑔𝑡)‘0) = (𝑥𝑡) ↔ ((𝑔𝑖)‘0) = (𝑥𝑖)))
6457fveq1d 6434 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑖 → ((𝑔𝑡)‘1) = ((𝑔𝑖)‘1))
65 fveq2 6432 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑖 → (𝑦𝑡) = (𝑦𝑖))
6664, 65eqeq12d 2839 . . . . . . . . . . . . . . 15 (𝑡 = 𝑖 → (((𝑔𝑡)‘1) = (𝑦𝑡) ↔ ((𝑔𝑖)‘1) = (𝑦𝑖)))
6763, 66anbi12d 626 . . . . . . . . . . . . . 14 (𝑡 = 𝑖 → ((((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡)) ↔ (((𝑔𝑖)‘0) = (𝑥𝑖) ∧ ((𝑔𝑖)‘1) = (𝑦𝑖))))
6860, 67anbi12d 626 . . . . . . . . . . . . 13 (𝑡 = 𝑖 → (((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))) ↔ ((𝑔𝑖) ∈ (II Cn (𝐹𝑖)) ∧ (((𝑔𝑖)‘0) = (𝑥𝑖) ∧ ((𝑔𝑖)‘1) = (𝑦𝑖)))))
6968rspccva 3524 . . . . . . . . . . . 12 ((∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))) ∧ 𝑖 ∈ ( I ‘𝐴)) → ((𝑔𝑖) ∈ (II Cn (𝐹𝑖)) ∧ (((𝑔𝑖)‘0) = (𝑥𝑖) ∧ ((𝑔𝑖)‘1) = (𝑦𝑖))))
7056, 69sylan 577 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖 ∈ ( I ‘𝐴)) → ((𝑔𝑖) ∈ (II Cn (𝐹𝑖)) ∧ (((𝑔𝑖)‘0) = (𝑥𝑖) ∧ ((𝑔𝑖)‘1) = (𝑦𝑖))))
7155, 70syldan 587 . . . . . . . . . 10 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → ((𝑔𝑖) ∈ (II Cn (𝐹𝑖)) ∧ (((𝑔𝑖)‘0) = (𝑥𝑖) ∧ ((𝑔𝑖)‘1) = (𝑦𝑖))))
7271simpld 490 . . . . . . . . 9 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → (𝑔𝑖) ∈ (II Cn (𝐹𝑖)))
73 iiuni 23053 . . . . . . . . . 10 (0[,]1) = II
74 eqid 2824 . . . . . . . . . 10 (𝐹𝑖) = (𝐹𝑖)
7573, 74cnf 21420 . . . . . . . . 9 ((𝑔𝑖) ∈ (II Cn (𝐹𝑖)) → (𝑔𝑖):(0[,]1)⟶ (𝐹𝑖))
7672, 75syl 17 . . . . . . . 8 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → (𝑔𝑖):(0[,]1)⟶ (𝐹𝑖))
7776feqmptd 6495 . . . . . . 7 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → (𝑔𝑖) = (𝑧 ∈ (0[,]1) ↦ ((𝑔𝑖)‘𝑧)))
7877, 72eqeltrrd 2906 . . . . . 6 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → (𝑧 ∈ (0[,]1) ↦ ((𝑔𝑖)‘𝑧)) ∈ (II Cn (𝐹𝑖)))
7914, 49, 50, 52, 78ptcn 21800 . . . . 5 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) ∈ (II Cn (∏t𝐹)))
8071simprd 491 . . . . . . . 8 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → (((𝑔𝑖)‘0) = (𝑥𝑖) ∧ ((𝑔𝑖)‘1) = (𝑦𝑖)))
8180simpld 490 . . . . . . 7 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → ((𝑔𝑖)‘0) = (𝑥𝑖))
8281mpteq2dva 4966 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → (𝑖𝐴 ↦ ((𝑔𝑖)‘0)) = (𝑖𝐴 ↦ (𝑥𝑖)))
83 0elunit 12580 . . . . . . 7 0 ∈ (0[,]1)
84 mptexg 6739 . . . . . . . 8 (𝐴𝑉 → (𝑖𝐴 ↦ ((𝑔𝑖)‘0)) ∈ V)
8550, 84syl 17 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → (𝑖𝐴 ↦ ((𝑔𝑖)‘0)) ∈ V)
86 fveq2 6432 . . . . . . . . 9 (𝑧 = 0 → ((𝑔𝑖)‘𝑧) = ((𝑔𝑖)‘0))
8786mpteq2dv 4967 . . . . . . . 8 (𝑧 = 0 → (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)) = (𝑖𝐴 ↦ ((𝑔𝑖)‘0)))
88 eqid 2824 . . . . . . . 8 (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) = (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))
8987, 88fvmptg 6526 . . . . . . 7 ((0 ∈ (0[,]1) ∧ (𝑖𝐴 ↦ ((𝑔𝑖)‘0)) ∈ V) → ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘0) = (𝑖𝐴 ↦ ((𝑔𝑖)‘0)))
9083, 85, 89sylancr 583 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘0) = (𝑖𝐴 ↦ ((𝑔𝑖)‘0)))
9121simpld 490 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑥 Fn 𝐴)
9291adantr 474 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → 𝑥 Fn 𝐴)
93 dffn5 6487 . . . . . . 7 (𝑥 Fn 𝐴𝑥 = (𝑖𝐴 ↦ (𝑥𝑖)))
9492, 93sylib 210 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → 𝑥 = (𝑖𝐴 ↦ (𝑥𝑖)))
9582, 90, 943eqtr4d 2870 . . . . 5 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘0) = 𝑥)
9680simprd 491 . . . . . . 7 (((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) ∧ 𝑖𝐴) → ((𝑔𝑖)‘1) = (𝑦𝑖))
9796mpteq2dva 4966 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → (𝑖𝐴 ↦ ((𝑔𝑖)‘1)) = (𝑖𝐴 ↦ (𝑦𝑖)))
98 1elunit 12581 . . . . . . 7 1 ∈ (0[,]1)
99 mptexg 6739 . . . . . . . 8 (𝐴𝑉 → (𝑖𝐴 ↦ ((𝑔𝑖)‘1)) ∈ V)
10050, 99syl 17 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → (𝑖𝐴 ↦ ((𝑔𝑖)‘1)) ∈ V)
101 fveq2 6432 . . . . . . . . 9 (𝑧 = 1 → ((𝑔𝑖)‘𝑧) = ((𝑔𝑖)‘1))
102101mpteq2dv 4967 . . . . . . . 8 (𝑧 = 1 → (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)) = (𝑖𝐴 ↦ ((𝑔𝑖)‘1)))
103102, 88fvmptg 6526 . . . . . . 7 ((1 ∈ (0[,]1) ∧ (𝑖𝐴 ↦ ((𝑔𝑖)‘1)) ∈ V) → ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘1) = (𝑖𝐴 ↦ ((𝑔𝑖)‘1)))
10498, 100, 103sylancr 583 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘1) = (𝑖𝐴 ↦ ((𝑔𝑖)‘1)))
10528simpld 490 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → 𝑦 Fn 𝐴)
106105adantr 474 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → 𝑦 Fn 𝐴)
107 dffn5 6487 . . . . . . 7 (𝑦 Fn 𝐴𝑦 = (𝑖𝐴 ↦ (𝑦𝑖)))
108106, 107sylib 210 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → 𝑦 = (𝑖𝐴 ↦ (𝑦𝑖)))
10997, 104, 1083eqtr4d 2870 . . . . 5 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘1) = 𝑦)
110 fveq1 6431 . . . . . . . 8 (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) → (𝑓‘0) = ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘0))
111110eqeq1d 2826 . . . . . . 7 (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) → ((𝑓‘0) = 𝑥 ↔ ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘0) = 𝑥))
112 fveq1 6431 . . . . . . . 8 (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) → (𝑓‘1) = ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘1))
113112eqeq1d 2826 . . . . . . 7 (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) → ((𝑓‘1) = 𝑦 ↔ ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘1) = 𝑦))
114111, 113anbi12d 626 . . . . . 6 (𝑓 = (𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ (((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘0) = 𝑥 ∧ ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘1) = 𝑦)))
115114rspcev 3525 . . . . 5 (((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧))) ∈ (II Cn (∏t𝐹)) ∧ (((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘0) = 𝑥 ∧ ((𝑧 ∈ (0[,]1) ↦ (𝑖𝐴 ↦ ((𝑔𝑖)‘𝑧)))‘1) = 𝑦)) → ∃𝑓 ∈ (II Cn (∏t𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))
11679, 95, 109, 115syl12anc 872 . . . 4 ((((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) ∧ (𝑔 Fn ( I ‘𝐴) ∧ ∀𝑡 ∈ ( I ‘𝐴)((𝑔𝑡) ∈ (II Cn (𝐹𝑡)) ∧ (((𝑔𝑡)‘0) = (𝑥𝑡) ∧ ((𝑔𝑡)‘1) = (𝑦𝑡))))) → ∃𝑓 ∈ (II Cn (∏t𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))
11747, 116exlimddv 2036 . . 3 (((𝐴𝑉𝐹:𝐴⟶PConn) ∧ (𝑥 (∏t𝐹) ∧ 𝑦 (∏t𝐹))) → ∃𝑓 ∈ (II Cn (∏t𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))
118117ralrimivva 3179 . 2 ((𝐴𝑉𝐹:𝐴⟶PConn) → ∀𝑥 (∏t𝐹)∀𝑦 (∏t𝐹)∃𝑓 ∈ (II Cn (∏t𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))
119 eqid 2824 . . 3 (∏t𝐹) = (∏t𝐹)
120119ispconn 31750 . 2 ((∏t𝐹) ∈ PConn ↔ ((∏t𝐹) ∈ Top ∧ ∀𝑥 (∏t𝐹)∀𝑦 (∏t𝐹)∃𝑓 ∈ (II Cn (∏t𝐹))((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
1216, 118, 120sylanbrc 580 1 ((𝐴𝑉𝐹:𝐴⟶PConn) → (∏t𝐹) ∈ PConn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wex 1880  wcel 2166  wral 3116  wrex 3117  Vcvv 3413  wss 3797   cuni 4657  cmpt 4951   I cid 5248   Fn wfn 6117  wf 6118  cfv 6122  (class class class)co 6904  Xcixp 8174  0cc0 10251  1c1 10252  [,]cicc 12465  tcpt 16451  Topctop 21067  TopOnctopon 21084   Cn ccn 21398  IIcii 23047  PConncpconn 31746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-rep 4993  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-reg 8765  ax-inf2 8814  ax-ac2 9599  ax-cnex 10307  ax-resscn 10308  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-addrcl 10312  ax-mulcl 10313  ax-mulrcl 10314  ax-mulcom 10315  ax-addass 10316  ax-mulass 10317  ax-distr 10318  ax-i2m1 10319  ax-1ne0 10320  ax-1rid 10321  ax-rnegex 10322  ax-rrecex 10323  ax-cnre 10324  ax-pre-lttri 10325  ax-pre-lttrn 10326  ax-pre-ltadd 10327  ax-pre-mulgt0 10328  ax-pre-sup 10329
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-int 4697  df-iun 4741  df-iin 4742  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-se 5301  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-isom 6131  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-om 7326  df-1st 7427  df-2nd 7428  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-1o 7825  df-oadd 7829  df-er 8008  df-map 8123  df-ixp 8175  df-en 8222  df-dom 8223  df-sdom 8224  df-fin 8225  df-fi 8585  df-sup 8616  df-inf 8617  df-r1 8903  df-rank 8904  df-card 9077  df-ac 9251  df-pnf 10392  df-mnf 10393  df-xr 10394  df-ltxr 10395  df-le 10396  df-sub 10586  df-neg 10587  df-div 11009  df-nn 11350  df-2 11413  df-3 11414  df-n0 11618  df-z 11704  df-uz 11968  df-q 12071  df-rp 12112  df-xneg 12231  df-xadd 12232  df-xmul 12233  df-icc 12469  df-seq 13095  df-exp 13154  df-cj 14215  df-re 14216  df-im 14217  df-sqrt 14351  df-abs 14352  df-topgen 16456  df-pt 16457  df-psmet 20097  df-xmet 20098  df-met 20099  df-bl 20100  df-mopn 20101  df-top 21068  df-topon 21085  df-bases 21120  df-cn 21401  df-cnp 21402  df-ii 23049  df-pconn 31748
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator