MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pt1hmeo Structured version   Visualization version   GIF version

Theorem pt1hmeo 23310
Description: The canonical homeomorphism from a topological product on a singleton to the topology of the factor. (Contributed by Mario Carneiro, 3-Feb-2015.) (Proof shortened by AV, 18-Apr-2021.)
Hypotheses
Ref Expression
pt1hmeo.j 𝐾 = (∏tβ€˜{⟨𝐴, 𝐽⟩})
pt1hmeo.a (πœ‘ β†’ 𝐴 ∈ 𝑉)
pt1hmeo.r (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
Assertion
Ref Expression
pt1hmeo (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) ∈ (𝐽Homeo𝐾))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐽   π‘₯,𝐾   πœ‘,π‘₯   π‘₯,𝑋
Allowed substitution hint:   𝑉(π‘₯)

Proof of Theorem pt1hmeo
Dummy variables π‘˜ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fconstmpt 5739 . . . . 5 ({𝐴} Γ— {π‘₯}) = (π‘˜ ∈ {𝐴} ↦ π‘₯)
2 pt1hmeo.a . . . . . . 7 (πœ‘ β†’ 𝐴 ∈ 𝑉)
32adantr 482 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ 𝑉)
4 sneq 4639 . . . . . . . . 9 (π‘˜ = 𝐴 β†’ {π‘˜} = {𝐴})
54xpeq1d 5706 . . . . . . . 8 (π‘˜ = 𝐴 β†’ ({π‘˜} Γ— {π‘₯}) = ({𝐴} Γ— {π‘₯}))
6 opeq1 4874 . . . . . . . . 9 (π‘˜ = 𝐴 β†’ βŸ¨π‘˜, π‘₯⟩ = ⟨𝐴, π‘₯⟩)
76sneqd 4641 . . . . . . . 8 (π‘˜ = 𝐴 β†’ {βŸ¨π‘˜, π‘₯⟩} = {⟨𝐴, π‘₯⟩})
85, 7eqeq12d 2749 . . . . . . 7 (π‘˜ = 𝐴 β†’ (({π‘˜} Γ— {π‘₯}) = {βŸ¨π‘˜, π‘₯⟩} ↔ ({𝐴} Γ— {π‘₯}) = {⟨𝐴, π‘₯⟩}))
9 vex 3479 . . . . . . . 8 π‘˜ ∈ V
10 vex 3479 . . . . . . . 8 π‘₯ ∈ V
119, 10xpsn 7139 . . . . . . 7 ({π‘˜} Γ— {π‘₯}) = {βŸ¨π‘˜, π‘₯⟩}
128, 11vtoclg 3557 . . . . . 6 (𝐴 ∈ 𝑉 β†’ ({𝐴} Γ— {π‘₯}) = {⟨𝐴, π‘₯⟩})
133, 12syl 17 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ({𝐴} Γ— {π‘₯}) = {⟨𝐴, π‘₯⟩})
141, 13eqtr3id 2787 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ {𝐴} ↦ π‘₯) = {⟨𝐴, π‘₯⟩})
1514mpteq2dva 5249 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ {𝐴} ↦ π‘₯)) = (π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}))
16 pt1hmeo.j . . . 4 𝐾 = (∏tβ€˜{⟨𝐴, 𝐽⟩})
17 pt1hmeo.r . . . 4 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
18 snex 5432 . . . . 5 {𝐴} ∈ V
1918a1i 11 . . . 4 (πœ‘ β†’ {𝐴} ∈ V)
20 topontop 22415 . . . . . 6 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
2117, 20syl 17 . . . . 5 (πœ‘ β†’ 𝐽 ∈ Top)
222, 21fsnd 6877 . . . 4 (πœ‘ β†’ {⟨𝐴, 𝐽⟩}:{𝐴}⟢Top)
2317cnmptid 23165 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ π‘₯) ∈ (𝐽 Cn 𝐽))
2423adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ {𝐴}) β†’ (π‘₯ ∈ 𝑋 ↦ π‘₯) ∈ (𝐽 Cn 𝐽))
25 elsni 4646 . . . . . . . 8 (π‘˜ ∈ {𝐴} β†’ π‘˜ = 𝐴)
2625fveq2d 6896 . . . . . . 7 (π‘˜ ∈ {𝐴} β†’ ({⟨𝐴, 𝐽⟩}β€˜π‘˜) = ({⟨𝐴, 𝐽⟩}β€˜π΄))
27 fvsng 7178 . . . . . . . 8 ((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOnβ€˜π‘‹)) β†’ ({⟨𝐴, 𝐽⟩}β€˜π΄) = 𝐽)
282, 17, 27syl2anc 585 . . . . . . 7 (πœ‘ β†’ ({⟨𝐴, 𝐽⟩}β€˜π΄) = 𝐽)
2926, 28sylan9eqr 2795 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ {𝐴}) β†’ ({⟨𝐴, 𝐽⟩}β€˜π‘˜) = 𝐽)
3029oveq2d 7425 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ {𝐴}) β†’ (𝐽 Cn ({⟨𝐴, 𝐽⟩}β€˜π‘˜)) = (𝐽 Cn 𝐽))
3124, 30eleqtrrd 2837 . . . 4 ((πœ‘ ∧ π‘˜ ∈ {𝐴}) β†’ (π‘₯ ∈ 𝑋 ↦ π‘₯) ∈ (𝐽 Cn ({⟨𝐴, 𝐽⟩}β€˜π‘˜)))
3216, 17, 19, 22, 31ptcn 23131 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ {𝐴} ↦ π‘₯)) ∈ (𝐽 Cn 𝐾))
3315, 32eqeltrrd 2835 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) ∈ (𝐽 Cn 𝐾))
34 simprr 772 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ 𝑦 = {⟨𝐴, π‘₯⟩})
3514adantrr 716 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ (π‘˜ ∈ {𝐴} ↦ π‘₯) = {⟨𝐴, π‘₯⟩})
3634, 35eqtr4d 2776 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ 𝑦 = (π‘˜ ∈ {𝐴} ↦ π‘₯))
37 simprl 770 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ π‘₯ ∈ 𝑋)
3837adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) ∧ π‘˜ ∈ {𝐴}) β†’ π‘₯ ∈ 𝑋)
3938fmpttd 7115 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ (π‘˜ ∈ {𝐴} ↦ π‘₯):{𝐴}βŸΆπ‘‹)
40 toponmax 22428 . . . . . . . . . . . 12 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 ∈ 𝐽)
4117, 40syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ 𝐽)
4241adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ 𝑋 ∈ 𝐽)
43 elmapg 8833 . . . . . . . . . 10 ((𝑋 ∈ 𝐽 ∧ {𝐴} ∈ V) β†’ ((π‘˜ ∈ {𝐴} ↦ π‘₯) ∈ (𝑋 ↑m {𝐴}) ↔ (π‘˜ ∈ {𝐴} ↦ π‘₯):{𝐴}βŸΆπ‘‹))
4442, 18, 43sylancl 587 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ ((π‘˜ ∈ {𝐴} ↦ π‘₯) ∈ (𝑋 ↑m {𝐴}) ↔ (π‘˜ ∈ {𝐴} ↦ π‘₯):{𝐴}βŸΆπ‘‹))
4539, 44mpbird 257 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ (π‘˜ ∈ {𝐴} ↦ π‘₯) ∈ (𝑋 ↑m {𝐴}))
4636, 45eqeltrd 2834 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ 𝑦 ∈ (𝑋 ↑m {𝐴}))
4734fveq1d 6894 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ (π‘¦β€˜π΄) = ({⟨𝐴, π‘₯⟩}β€˜π΄))
482adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ 𝐴 ∈ 𝑉)
49 fvsng 7178 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ π‘₯ ∈ 𝑋) β†’ ({⟨𝐴, π‘₯⟩}β€˜π΄) = π‘₯)
5048, 37, 49syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ ({⟨𝐴, π‘₯⟩}β€˜π΄) = π‘₯)
5147, 50eqtr2d 2774 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ π‘₯ = (π‘¦β€˜π΄))
5246, 51jca 513 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩})) β†’ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄)))
53 simprr 772 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ π‘₯ = (π‘¦β€˜π΄))
54 simprl 770 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ 𝑦 ∈ (𝑋 ↑m {𝐴}))
5541adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ 𝑋 ∈ 𝐽)
56 elmapg 8833 . . . . . . . . . . 11 ((𝑋 ∈ 𝐽 ∧ {𝐴} ∈ V) β†’ (𝑦 ∈ (𝑋 ↑m {𝐴}) ↔ 𝑦:{𝐴}βŸΆπ‘‹))
5755, 18, 56sylancl 587 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ (𝑦 ∈ (𝑋 ↑m {𝐴}) ↔ 𝑦:{𝐴}βŸΆπ‘‹))
5854, 57mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ 𝑦:{𝐴}βŸΆπ‘‹)
59 snidg 4663 . . . . . . . . . . 11 (𝐴 ∈ 𝑉 β†’ 𝐴 ∈ {𝐴})
602, 59syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ {𝐴})
6160adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ 𝐴 ∈ {𝐴})
6258, 61ffvelcdmd 7088 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ (π‘¦β€˜π΄) ∈ 𝑋)
6353, 62eqeltrd 2834 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ π‘₯ ∈ 𝑋)
642adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ 𝐴 ∈ 𝑉)
65 fsn2g 7136 . . . . . . . . . . 11 (𝐴 ∈ 𝑉 β†’ (𝑦:{𝐴}βŸΆπ‘‹ ↔ ((π‘¦β€˜π΄) ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, (π‘¦β€˜π΄)⟩})))
6664, 65syl 17 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ (𝑦:{𝐴}βŸΆπ‘‹ ↔ ((π‘¦β€˜π΄) ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, (π‘¦β€˜π΄)⟩})))
6758, 66mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ ((π‘¦β€˜π΄) ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, (π‘¦β€˜π΄)⟩}))
6867simprd 497 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ 𝑦 = {⟨𝐴, (π‘¦β€˜π΄)⟩})
6953opeq2d 4881 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ ⟨𝐴, π‘₯⟩ = ⟨𝐴, (π‘¦β€˜π΄)⟩)
7069sneqd 4641 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ {⟨𝐴, π‘₯⟩} = {⟨𝐴, (π‘¦β€˜π΄)⟩})
7168, 70eqtr4d 2776 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ 𝑦 = {⟨𝐴, π‘₯⟩})
7263, 71jca 513 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))) β†’ (π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩}))
7352, 72impbida 800 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ∧ 𝑦 = {⟨𝐴, π‘₯⟩}) ↔ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ π‘₯ = (π‘¦β€˜π΄))))
7473mptcnv 6140 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) = (𝑦 ∈ (𝑋 ↑m {𝐴}) ↦ (π‘¦β€˜π΄)))
75 xpsng 7137 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOnβ€˜π‘‹)) β†’ ({𝐴} Γ— {𝐽}) = {⟨𝐴, 𝐽⟩})
762, 17, 75syl2anc 585 . . . . . . . . . 10 (πœ‘ β†’ ({𝐴} Γ— {𝐽}) = {⟨𝐴, 𝐽⟩})
7776eqcomd 2739 . . . . . . . . 9 (πœ‘ β†’ {⟨𝐴, 𝐽⟩} = ({𝐴} Γ— {𝐽}))
7877fveq2d 6896 . . . . . . . 8 (πœ‘ β†’ (∏tβ€˜{⟨𝐴, 𝐽⟩}) = (∏tβ€˜({𝐴} Γ— {𝐽})))
7916, 78eqtrid 2785 . . . . . . 7 (πœ‘ β†’ 𝐾 = (∏tβ€˜({𝐴} Γ— {𝐽})))
80 eqid 2733 . . . . . . . . 9 (∏tβ€˜({𝐴} Γ— {𝐽})) = (∏tβ€˜({𝐴} Γ— {𝐽}))
8180pttoponconst 23101 . . . . . . . 8 (({𝐴} ∈ V ∧ 𝐽 ∈ (TopOnβ€˜π‘‹)) β†’ (∏tβ€˜({𝐴} Γ— {𝐽})) ∈ (TopOnβ€˜(𝑋 ↑m {𝐴})))
8219, 17, 81syl2anc 585 . . . . . . 7 (πœ‘ β†’ (∏tβ€˜({𝐴} Γ— {𝐽})) ∈ (TopOnβ€˜(𝑋 ↑m {𝐴})))
8379, 82eqeltrd 2834 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜(𝑋 ↑m {𝐴})))
84 toponuni 22416 . . . . . 6 (𝐾 ∈ (TopOnβ€˜(𝑋 ↑m {𝐴})) β†’ (𝑋 ↑m {𝐴}) = βˆͺ 𝐾)
8583, 84syl 17 . . . . 5 (πœ‘ β†’ (𝑋 ↑m {𝐴}) = βˆͺ 𝐾)
8685mpteq1d 5244 . . . 4 (πœ‘ β†’ (𝑦 ∈ (𝑋 ↑m {𝐴}) ↦ (π‘¦β€˜π΄)) = (𝑦 ∈ βˆͺ 𝐾 ↦ (π‘¦β€˜π΄)))
8774, 86eqtrd 2773 . . 3 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) = (𝑦 ∈ βˆͺ 𝐾 ↦ (π‘¦β€˜π΄)))
88 eqid 2733 . . . . . 6 βˆͺ 𝐾 = βˆͺ 𝐾
8988, 16ptpjcn 23115 . . . . 5 (({𝐴} ∈ V ∧ {⟨𝐴, 𝐽⟩}:{𝐴}⟢Top ∧ 𝐴 ∈ {𝐴}) β†’ (𝑦 ∈ βˆͺ 𝐾 ↦ (π‘¦β€˜π΄)) ∈ (𝐾 Cn ({⟨𝐴, 𝐽⟩}β€˜π΄)))
9018, 22, 60, 89mp3an2i 1467 . . . 4 (πœ‘ β†’ (𝑦 ∈ βˆͺ 𝐾 ↦ (π‘¦β€˜π΄)) ∈ (𝐾 Cn ({⟨𝐴, 𝐽⟩}β€˜π΄)))
9128oveq2d 7425 . . . 4 (πœ‘ β†’ (𝐾 Cn ({⟨𝐴, 𝐽⟩}β€˜π΄)) = (𝐾 Cn 𝐽))
9290, 91eleqtrd 2836 . . 3 (πœ‘ β†’ (𝑦 ∈ βˆͺ 𝐾 ↦ (π‘¦β€˜π΄)) ∈ (𝐾 Cn 𝐽))
9387, 92eqeltrd 2834 . 2 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) ∈ (𝐾 Cn 𝐽))
94 ishmeo 23263 . 2 ((π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) ∈ (𝐽Homeo𝐾) ↔ ((π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) ∈ (𝐽 Cn 𝐾) ∧ β—‘(π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) ∈ (𝐾 Cn 𝐽)))
9533, 93, 94sylanbrc 584 1 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ {⟨𝐴, π‘₯⟩}) ∈ (𝐽Homeo𝐾))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4629  βŸ¨cop 4635  βˆͺ cuni 4909   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ↑m cmap 8820  βˆtcpt 17384  Topctop 22395  TopOnctopon 22412   Cn ccn 22728  Homeochmeo 23257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9406  df-topgen 17389  df-pt 17390  df-top 22396  df-topon 22413  df-bases 22449  df-cn 22731  df-cnp 22732  df-hmeo 23259
This theorem is referenced by:  xpstopnlem1  23313  ptcmpfi  23317
  Copyright terms: Public domain W3C validator