ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  neitx GIF version
Theorem neitx 13771
Description: The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
Hypotheses
Ref Expression
neitx.x 𝑋 = βˆͺ 𝐽
neitx.y π‘Œ = βˆͺ 𝐾
Assertion
Ref Expression
neitx (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝐴 Γ— 𝐡) ∈ ((neiβ€˜(𝐽 Γ—t 𝐾))β€˜(𝐢 Γ— 𝐷)))
Proof of Theorem neitx
Dummy variables π‘Ž 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neitx.x . . . . . 6 𝑋 = βˆͺ 𝐽
21neii1 13650 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴 ∈ ((neiβ€˜π½)β€˜πΆ)) β†’ 𝐴 βŠ† 𝑋)
32ad2ant2r 509 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ 𝐴 βŠ† 𝑋)
4 neitx.y . . . . . 6 π‘Œ = βˆͺ 𝐾
54neii1 13650 . . . . 5 ((𝐾 ∈ Top ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·)) β†’ 𝐡 βŠ† π‘Œ)
65ad2ant2l 508 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ 𝐡 βŠ† π‘Œ)
7 xpss12 4734 . . . 4 ((𝐴 βŠ† 𝑋 ∧ 𝐡 βŠ† π‘Œ) β†’ (𝐴 Γ— 𝐡) βŠ† (𝑋 Γ— π‘Œ))
83, 6, 7syl2anc 411 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝐴 Γ— 𝐡) βŠ† (𝑋 Γ— π‘Œ))
91, 4txuni 13766 . . . 4 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) β†’ (𝑋 Γ— π‘Œ) = βˆͺ (𝐽 Γ—t 𝐾))
109adantr 276 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝑋 Γ— π‘Œ) = βˆͺ (𝐽 Γ—t 𝐾))
118, 10sseqtrd 3194 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝐴 Γ— 𝐡) βŠ† βˆͺ (𝐽 Γ—t 𝐾))
12 simp-5l 543 . . . . . 6 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
13 simp-4r 542 . . . . . 6 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ π‘Ž ∈ 𝐽)
14 simplr 528 . . . . . 6 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ 𝑏 ∈ 𝐾)
15 txopn 13768 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (π‘Ž ∈ 𝐽 ∧ 𝑏 ∈ 𝐾)) β†’ (π‘Ž Γ— 𝑏) ∈ (𝐽 Γ—t 𝐾))
1612, 13, 14, 15syl12anc 1236 . . . . 5 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ (π‘Ž Γ— 𝑏) ∈ (𝐽 Γ—t 𝐾))
17 simpr1l 1054 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ ((𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡))) β†’ 𝐢 βŠ† π‘Ž)
18173anassrs 1229 . . . . . 6 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ 𝐢 βŠ† π‘Ž)
19 simprl 529 . . . . . 6 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ 𝐷 βŠ† 𝑏)
20 xpss12 4734 . . . . . 6 ((𝐢 βŠ† π‘Ž ∧ 𝐷 βŠ† 𝑏) β†’ (𝐢 Γ— 𝐷) βŠ† (π‘Ž Γ— 𝑏))
2118, 19, 20syl2anc 411 . . . . 5 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ (𝐢 Γ— 𝐷) βŠ† (π‘Ž Γ— 𝑏))
22 simpr1r 1055 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ ((𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡))) β†’ π‘Ž βŠ† 𝐴)
23223anassrs 1229 . . . . . 6 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ π‘Ž βŠ† 𝐴)
24 simprr 531 . . . . . 6 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ 𝑏 βŠ† 𝐡)
25 xpss12 4734 . . . . . 6 ((π‘Ž βŠ† 𝐴 ∧ 𝑏 βŠ† 𝐡) β†’ (π‘Ž Γ— 𝑏) βŠ† (𝐴 Γ— 𝐡))
2623, 24, 25syl2anc 411 . . . . 5 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ (π‘Ž Γ— 𝑏) βŠ† (𝐴 Γ— 𝐡))
27 sseq2 3180 . . . . . . 7 (𝑐 = (π‘Ž Γ— 𝑏) β†’ ((𝐢 Γ— 𝐷) βŠ† 𝑐 ↔ (𝐢 Γ— 𝐷) βŠ† (π‘Ž Γ— 𝑏)))
28 sseq1 3179 . . . . . . 7 (𝑐 = (π‘Ž Γ— 𝑏) β†’ (𝑐 βŠ† (𝐴 Γ— 𝐡) ↔ (π‘Ž Γ— 𝑏) βŠ† (𝐴 Γ— 𝐡)))
2927, 28anbi12d 473 . . . . . 6 (𝑐 = (π‘Ž Γ— 𝑏) β†’ (((𝐢 Γ— 𝐷) βŠ† 𝑐 ∧ 𝑐 βŠ† (𝐴 Γ— 𝐡)) ↔ ((𝐢 Γ— 𝐷) βŠ† (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐴 Γ— 𝐡))))
3029rspcev 2842 . . . . 5 (((π‘Ž Γ— 𝑏) ∈ (𝐽 Γ—t 𝐾) ∧ ((𝐢 Γ— 𝐷) βŠ† (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐴 Γ— 𝐡))) β†’ βˆƒπ‘ ∈ (𝐽 Γ—t 𝐾)((𝐢 Γ— 𝐷) βŠ† 𝑐 ∧ 𝑐 βŠ† (𝐴 Γ— 𝐡)))
3116, 21, 26, 30syl12anc 1236 . . . 4 (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡)) β†’ βˆƒπ‘ ∈ (𝐽 Γ—t 𝐾)((𝐢 Γ— 𝐷) βŠ† 𝑐 ∧ 𝑐 βŠ† (𝐴 Γ— 𝐡)))
32 neii2 13652 . . . . . 6 ((𝐾 ∈ Top ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·)) β†’ βˆƒπ‘ ∈ 𝐾 (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡))
3332ad2ant2l 508 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ βˆƒπ‘ ∈ 𝐾 (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡))
3433ad2antrr 488 . . . 4 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) β†’ βˆƒπ‘ ∈ 𝐾 (𝐷 βŠ† 𝑏 ∧ 𝑏 βŠ† 𝐡))
3531, 34r19.29a 2620 . . 3 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) ∧ π‘Ž ∈ 𝐽) ∧ (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴)) β†’ βˆƒπ‘ ∈ (𝐽 Γ—t 𝐾)((𝐢 Γ— 𝐷) βŠ† 𝑐 ∧ 𝑐 βŠ† (𝐴 Γ— 𝐡)))
36 neii2 13652 . . . 4 ((𝐽 ∈ Top ∧ 𝐴 ∈ ((neiβ€˜π½)β€˜πΆ)) β†’ βˆƒπ‘Ž ∈ 𝐽 (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴))
3736ad2ant2r 509 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ βˆƒπ‘Ž ∈ 𝐽 (𝐢 βŠ† π‘Ž ∧ π‘Ž βŠ† 𝐴))
3835, 37r19.29a 2620 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ βˆƒπ‘ ∈ (𝐽 Γ—t 𝐾)((𝐢 Γ— 𝐷) βŠ† 𝑐 ∧ 𝑐 βŠ† (𝐴 Γ— 𝐡)))
39 txtop 13763 . . . 4 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) β†’ (𝐽 Γ—t 𝐾) ∈ Top)
4039adantr 276 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝐽 Γ—t 𝐾) ∈ Top)
411neiss2 13645 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐴 ∈ ((neiβ€˜π½)β€˜πΆ)) β†’ 𝐢 βŠ† 𝑋)
4241ad2ant2r 509 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ 𝐢 βŠ† 𝑋)
434neiss2 13645 . . . . . 6 ((𝐾 ∈ Top ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·)) β†’ 𝐷 βŠ† π‘Œ)
4443ad2ant2l 508 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ 𝐷 βŠ† π‘Œ)
45 xpss12 4734 . . . . 5 ((𝐢 βŠ† 𝑋 ∧ 𝐷 βŠ† π‘Œ) β†’ (𝐢 Γ— 𝐷) βŠ† (𝑋 Γ— π‘Œ))
4642, 44, 45syl2anc 411 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝐢 Γ— 𝐷) βŠ† (𝑋 Γ— π‘Œ))
4746, 10sseqtrd 3194 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝐢 Γ— 𝐷) βŠ† βˆͺ (𝐽 Γ—t 𝐾))
48 eqid 2177 . . . 4 βˆͺ (𝐽 Γ—t 𝐾) = βˆͺ (𝐽 Γ—t 𝐾)
4948isnei 13647 . . 3 (((𝐽 Γ—t 𝐾) ∈ Top ∧ (𝐢 Γ— 𝐷) βŠ† βˆͺ (𝐽 Γ—t 𝐾)) β†’ ((𝐴 Γ— 𝐡) ∈ ((neiβ€˜(𝐽 Γ—t 𝐾))β€˜(𝐢 Γ— 𝐷)) ↔ ((𝐴 Γ— 𝐡) βŠ† βˆͺ (𝐽 Γ—t 𝐾) ∧ βˆƒπ‘ ∈ (𝐽 Γ—t 𝐾)((𝐢 Γ— 𝐷) βŠ† 𝑐 ∧ 𝑐 βŠ† (𝐴 Γ— 𝐡)))))
5040, 47, 49syl2anc 411 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ ((𝐴 Γ— 𝐡) ∈ ((neiβ€˜(𝐽 Γ—t 𝐾))β€˜(𝐢 Γ— 𝐷)) ↔ ((𝐴 Γ— 𝐡) βŠ† βˆͺ (𝐽 Γ—t 𝐾) ∧ βˆƒπ‘ ∈ (𝐽 Γ—t 𝐾)((𝐢 Γ— 𝐷) βŠ† 𝑐 ∧ 𝑐 βŠ† (𝐴 Γ— 𝐡)))))
5111, 38, 50mpbir2and 944 1 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((neiβ€˜π½)β€˜πΆ) ∧ 𝐡 ∈ ((neiβ€˜πΎ)β€˜π·))) β†’ (𝐴 Γ— 𝐡) ∈ ((neiβ€˜(𝐽 Γ—t 𝐾))β€˜(𝐢 Γ— 𝐷)))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  βˆƒwrex 2456   βŠ† wss 3130  βˆͺ cuni 3810   Γ— cxp 4625  β€˜cfv 5217  (class class class)co 5875  Topctop 13500  neicnei 13641   Γ—t ctx 13755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-topgen 12709  df-top 13501  df-topon 13514  df-bases 13546  df-nei 13642  df-tx 13756
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator