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

Theorem nllyrest 21813
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 21800 . . 3 (𝐽 ∈ 𝑛-Locally 𝐴𝐽 ∈ Top)
2 resttop 21487 . . 3 ((𝐽 ∈ Top ∧ 𝐵𝐽) → (𝐽t 𝐵) ∈ Top)
31, 2sylan 572 . 2 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝐽t 𝐵) ∈ Top)
4 restopn2 21504 . . . . 5 ((𝐽 ∈ Top ∧ 𝐵𝐽) → (𝑥 ∈ (𝐽t 𝐵) ↔ (𝑥𝐽𝑥𝐵)))
51, 4sylan 572 . . . 4 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝑥 ∈ (𝐽t 𝐵) ↔ (𝑥𝐽𝑥𝐵)))
6 simp1l 1178 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → 𝐽 ∈ 𝑛-Locally 𝐴)
7 simp2l 1180 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → 𝑥𝐽)
8 simp3 1119 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → 𝑦𝑥)
9 nlly2i 21803 . . . . . . . . 9 ((𝐽 ∈ 𝑛-Locally 𝐴𝑥𝐽𝑦𝑥) → ∃𝑠 ∈ 𝒫 𝑥𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))
106, 7, 8, 9syl3anc 1352 . . . . . . . 8 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → ∃𝑠 ∈ 𝒫 𝑥𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))
1133ad2ant1 1114 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → (𝐽t 𝐵) ∈ Top)
12113ad2ant1 1114 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝐽t 𝐵) ∈ Top)
13 simp3l 1182 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢𝐽)
14 simp3r2 1263 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢𝑠)
15 simp2 1118 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 ∈ 𝒫 𝑥)
1615elpwid 4437 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠𝑥)
17 simp12r 1268 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑥𝐵)
1816, 17sstrd 3870 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠𝐵)
1914, 18sstrd 3870 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢𝐵)
2063ad2ant1 1114 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐽 ∈ 𝑛-Locally 𝐴)
2120, 1syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐽 ∈ Top)
22 simp11r 1266 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐵𝐽)
23 restopn2 21504 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝐵𝐽) → (𝑢 ∈ (𝐽t 𝐵) ↔ (𝑢𝐽𝑢𝐵)))
2421, 22, 23syl2anc 576 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝑢 ∈ (𝐽t 𝐵) ↔ (𝑢𝐽𝑢𝐵)))
2513, 19, 24mpbir2and 701 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢 ∈ (𝐽t 𝐵))
26 simp3r1 1262 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑦𝑢)
27 opnneip 21446 . . . . . . . . . . . . . . . 16 (((𝐽t 𝐵) ∈ Top ∧ 𝑢 ∈ (𝐽t 𝐵) ∧ 𝑦𝑢) → 𝑢 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
2812, 25, 26, 27syl3anc 1352 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑢 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
29 elssuni 4746 . . . . . . . . . . . . . . . . . 18 (𝐵𝐽𝐵 𝐽)
3022, 29syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐵 𝐽)
31 eqid 2780 . . . . . . . . . . . . . . . . . 18 𝐽 = 𝐽
3231restuni 21489 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝐵 𝐽) → 𝐵 = (𝐽t 𝐵))
3321, 30, 32syl2anc 576 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝐵 = (𝐽t 𝐵))
3418, 33sseqtrd 3899 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 (𝐽t 𝐵))
35 eqid 2780 . . . . . . . . . . . . . . . 16 (𝐽t 𝐵) = (𝐽t 𝐵)
3635ssnei2 21443 . . . . . . . . . . . . . . 15 ((((𝐽t 𝐵) ∈ Top ∧ 𝑢 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦})) ∧ (𝑢𝑠𝑠 (𝐽t 𝐵))) → 𝑠 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
3712, 28, 14, 34, 36syl22anc 827 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 ∈ ((nei‘(𝐽t 𝐵))‘{𝑦}))
3837, 15elind 4062 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → 𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥))
39 restabs 21492 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑠𝐵𝐵𝐽) → ((𝐽t 𝐵) ↾t 𝑠) = (𝐽t 𝑠))
4021, 18, 22, 39syl3anc 1352 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → ((𝐽t 𝐵) ↾t 𝑠) = (𝐽t 𝑠))
41 simp3r3 1264 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝐽t 𝑠) ∈ 𝐴)
4240, 41eqeltrd 2868 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
4338, 42jca 504 . . . . . . . . . . . 12 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥 ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
44433expa 1099 . . . . . . . . . . 11 (((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥) ∧ (𝑢𝐽 ∧ (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴))) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
4544rexlimdvaa 3232 . . . . . . . . . 10 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) ∧ 𝑠 ∈ 𝒫 𝑥) → (∃𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)))
4645expimpd 446 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → ((𝑠 ∈ 𝒫 𝑥 ∧ ∃𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴)) → (𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)))
4746reximdv2 3218 . . . . . . . 8 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → (∃𝑠 ∈ 𝒫 𝑥𝑢𝐽 (𝑦𝑢𝑢𝑠 ∧ (𝐽t 𝑠) ∈ 𝐴) → ∃𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
4810, 47mpd 15 . . . . . . 7 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵) ∧ 𝑦𝑥) → ∃𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
49483expa 1099 . . . . . 6 ((((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵)) ∧ 𝑦𝑥) → ∃𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
5049ralrimiva 3134 . . . . 5 (((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) ∧ (𝑥𝐽𝑥𝐵)) → ∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
5150ex 405 . . . 4 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → ((𝑥𝐽𝑥𝐵) → ∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
525, 51sylbid 232 . . 3 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝑥 ∈ (𝐽t 𝐵) → ∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
5352ralrimiv 3133 . 2 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → ∀𝑥 ∈ (𝐽t 𝐵)∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴)
54 isnlly 21796 . 2 ((𝐽t 𝐵) ∈ 𝑛-Locally 𝐴 ↔ ((𝐽t 𝐵) ∈ Top ∧ ∀𝑥 ∈ (𝐽t 𝐵)∀𝑦𝑥𝑠 ∈ (((nei‘(𝐽t 𝐵))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐵) ↾t 𝑠) ∈ 𝐴))
553, 53, 54sylanbrc 575 1 ((𝐽 ∈ 𝑛-Locally 𝐴𝐵𝐽) → (𝐽t 𝐵) ∈ 𝑛-Locally 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051  wral 3090  wrex 3091  cin 3830  wss 3831  𝒫 cpw 4425  {csn 4444   cuni 4717  cfv 6193  (class class class)co 6982  t crest 16556  Topctop 21220  neicnei 21424  𝑛-Locally cnlly 21792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-tp 4449  df-op 4451  df-uni 4718  df-int 4755  df-iun 4799  df-br 4935  df-opab 4997  df-mpt 5014  df-tr 5036  df-id 5316  df-eprel 5321  df-po 5330  df-so 5331  df-fr 5370  df-we 5372  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-pred 5991  df-ord 6037  df-on 6038  df-lim 6039  df-suc 6040  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-ov 6985  df-oprab 6986  df-mpo 6987  df-om 7403  df-1st 7507  df-2nd 7508  df-wrecs 7756  df-recs 7818  df-rdg 7856  df-oadd 7915  df-er 8095  df-en 8313  df-fin 8316  df-fi 8676  df-rest 16558  df-topgen 16579  df-top 21221  df-topon 21238  df-bases 21273  df-nei 21425  df-nlly 21794
This theorem is referenced by:  loclly  21814  nllyidm  21816
  Copyright terms: Public domain W3C validator