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

Theorem nllyrest 21208
Description: An open subspace of an n-locally 𝐴 space is also n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
nllyrest ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝐽t 𝐵) ∈ 𝑛-Locally 𝐴)

Proof of Theorem nllyrest
Dummy variables 𝑠 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nllytop 21195 . . 3 (𝐽 ∈ 𝑛-Locally 𝐴𝐽 ∈ Top)
2 resttop 20883 . . 3 ((𝐽 ∈ Top ∧ 𝐵𝐽) → (𝐽t 𝐵) ∈ Top)
31, 2sylan 488 . 2 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝐽t 𝐵) ∈ Top)
4 restopn2 20900 . . . . 5 ((𝐽 ∈ Top ∧ 𝐵𝐽) → (𝑥 ∈ (𝐽t 𝐵) ↔ (𝑥𝐽𝑥𝐵)))
51, 4sylan 488 . . . 4 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝑥 ∈ (𝐽t 𝐵) ↔ (𝑥𝐽𝑥𝐵)))
6 simp1l 1083 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → 𝐽 ∈ 𝑛-Locally 𝐴)
7 simp2l 1085 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → 𝑥𝐽)
8 simp3 1061 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → 𝑦𝑥)
9 nlly2i 21198 . . . . . . . . 9 ((𝐽 ∈ 𝑛-Locally 𝐴𝑥𝐽𝑦𝑥) → ∃𝑠 ∈ 𝒫 𝑥𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))
106, 7, 8, 9syl3anc 1323 . . . . . . . 8 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → ∃𝑠 ∈ 𝒫 𝑥𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))
1133ad2ant1 1080 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → (𝐽t 𝐵) ∈ Top)
12113ad2ant1 1080 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝐽t 𝐵) ∈ Top)
13 simp3l 1087 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢𝐽)
14 simp3r2 1168 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢𝑠)
15 simp2 1060 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 ∈ 𝒫 𝑥)
1615elpwid 4146 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠𝑥)
17 simp12r 1173 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑥𝐵)
1816, 17sstrd 3597 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠𝐵)
1914, 18sstrd 3597 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢𝐵)
2063ad2ant1 1080 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐽 ∈ 𝑛-Locally 𝐴)
2120, 1syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐽 ∈ Top)
22 simp11r 1171 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐵𝐽)
23 restopn2 20900 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝐵𝐽) → (𝑢 ∈ (𝐽t 𝐵) ↔ (𝑢𝐽𝑢𝐵)))
2421, 22, 23syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝑢 ∈ (𝐽t 𝐵) ↔ (𝑢𝐽𝑢𝐵)))
2513, 19, 24mpbir2and 956 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢 ∈ (𝐽t 𝐵))
26 simp3r1 1167 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑦𝑢)
27 opnneip 20842 . . . . . . . . . . . . . . . 16 (((𝐽t 𝐵) ∈ Top ∧ 𝑢 ∈ (𝐽t 𝐵) ∧ 𝑦𝑢) → 𝑢 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
2812, 25, 26, 27syl3anc 1323 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
29 elssuni 4438 . . . . . . . . . . . . . . . . . 18 (𝐵𝐽𝐵 𝐽)
3022, 29syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐵 𝐽)
31 eqid 2621 . . . . . . . . . . . . . . . . . 18 𝐽 = 𝐽
3231restuni 20885 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝐵 𝐽) → 𝐵 = (𝐽t 𝐵))
3321, 30, 32syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐵 = (𝐽t 𝐵))
3418, 33sseqtrd 3625 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 (𝐽t 𝐵))
35 eqid 2621 . . . . . . . . . . . . . . . 16 (𝐽t 𝐵) = (𝐽t 𝐵)
3635ssnei2 20839 . . . . . . . . . . . . . . 15 ((((𝐽t 𝐵) ∈ Top ∧ 𝑢 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦})) ∧ (𝑢𝑠𝑠 (𝐽t 𝐵))) → 𝑠 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
3712, 28, 14, 34, 36syl22anc 1324 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
3837, 15elind 3781 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥))
39 restabs 20888 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑠𝐵𝐵𝐽) → ((𝐽t 𝐵) ↾t 𝑠) = (𝐽t 𝑠))
4021, 18, 22, 39syl3anc 1323 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → ((𝐽t 𝐵) ↾t 𝑠) = (𝐽t 𝑠))
41 simp3r3 1169 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝐽t 𝑠) ∈ 𝐴)
4240, 41eqeltrd 2698 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
4338, 42jca 554 . . . . . . . . . . . 12 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
44433expa 1262 . . . . . . . . . . 11 (((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥) ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
4544rexlimdvaa 3026 . . . . . . . . . 10 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥) → (∃𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)))
4645expimpd 628 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → ((𝑠 ∈ 𝒫 𝑥 ∧ ∃𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴)) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)))
4746reximdv2 3009 . . . . . . . 8 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → (∃𝑠 ∈ 𝒫 𝑥𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴) → ∃𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
4810, 47mpd 15 . . . . . . 7 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → ∃𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
49483expa 1262 . . . . . 6 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵)) ∧ 𝑦𝑥) → ∃𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
5049ralrimiva 2961 . . . . 5 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵)) → ∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
5150ex 450 . . . 4 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → ((𝑥𝐽𝑥𝐵) → ∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
525, 51sylbid 230 . . 3 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝑥 ∈ (𝐽t 𝐵) → ∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
5352ralrimiv 2960 . 2 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → ∀𝑥 ∈ (𝐽t 𝐵)∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
54 isnlly 21191 . 2 ((𝐽t 𝐵) ∈ 𝑛-Locally 𝐴 ↔ ((𝐽t 𝐵) ∈ Top ∧ ∀𝑥 ∈ (𝐽t 𝐵)∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
553, 53, 54sylanbrc 697 1 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝐽t 𝐵) ∈ 𝑛-Locally 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  cin 3558  wss 3559  𝒫 cpw 4135  {csn 4153   cuni 4407  cfv 5852  (class class class)co 6610  t crest 16009  Topctop 20626  neicnei 20820  𝑛-Locally cnlly 21187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-oadd 7516  df-er 7694  df-en 7907  df-fin 7910  df-fi 8268  df-rest 16011  df-topgen 16032  df-top 20627  df-topon 20644  df-bases 20670  df-nei 20821  df-nlly 21189
This theorem is referenced by:  loclly  21209  nllyidm  21211
  Copyright terms: Public domain W3C validator