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

Theorem neiptopnei 21741
Description: Lemma for neiptopreu 21742. (Contributed by Thierry Arnoux, 7-Jan-2018.)
Hypotheses
Ref Expression
neiptop.o 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝𝑎 𝑎 ∈ (𝑁𝑝)}
neiptop.0 (𝜑𝑁:𝑋⟶𝒫 𝒫 𝑋)
neiptop.1 ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
neiptop.2 ((𝜑𝑝𝑋) → (fi‘(𝑁𝑝)) ⊆ (𝑁𝑝))
neiptop.3 (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑝𝑎)
neiptop.4 (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
neiptop.5 ((𝜑𝑝𝑋) → 𝑋 ∈ (𝑁𝑝))
Assertion
Ref Expression
neiptopnei (𝜑𝑁 = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Distinct variable groups:   𝑝,𝑎,𝑁   𝑋,𝑎,𝑏,𝑝   𝐽,𝑎,𝑝   𝑋,𝑝   𝜑,𝑝   𝑁,𝑏   𝑋,𝑏   𝜑,𝑎,𝑏,𝑞,𝑝   𝑁,𝑝,𝑞   𝑋,𝑞   𝜑,𝑞
Allowed substitution hints:   𝐽(𝑞,𝑏)

Proof of Theorem neiptopnei
Dummy variables 𝑐 𝑑 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neiptop.0 . . 3 (𝜑𝑁:𝑋⟶𝒫 𝒫 𝑋)
21feqmptd 6712 . 2 (𝜑𝑁 = (𝑝𝑋 ↦ (𝑁𝑝)))
31ffvelrnda 6832 . . . . . . . . . . . 12 ((𝜑𝑝𝑋) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
43adantr 484 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
54elpwid 4511 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ⊆ 𝒫 𝑋)
6 simpr 488 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
75, 6sseldd 3919 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ 𝒫 𝑋)
87elpwid 4511 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐𝑋)
9 neiptop.o . . . . . . . . . . 11 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝𝑎 𝑎 ∈ (𝑁𝑝)}
10 neiptop.1 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
11 neiptop.2 . . . . . . . . . . 11 ((𝜑𝑝𝑋) → (fi‘(𝑁𝑝)) ⊆ (𝑁𝑝))
12 neiptop.3 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑝𝑎)
13 neiptop.4 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
14 neiptop.5 . . . . . . . . . . 11 ((𝜑𝑝𝑋) → 𝑋 ∈ (𝑁𝑝))
159, 1, 10, 11, 12, 13, 14neiptopuni 21739 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1615adantr 484 . . . . . . . . 9 ((𝜑𝑝𝑋) → 𝑋 = 𝐽)
1716adantr 484 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑋 = 𝐽)
188, 17sseqtrd 3958 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 𝐽)
19 ssrab2 4010 . . . . . . . . . 10 {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋
2019a1i 11 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)
21 fveq2 6649 . . . . . . . . . . . . . 14 (𝑞 = 𝑟 → (𝑁𝑞) = (𝑁𝑟))
2221eleq2d 2878 . . . . . . . . . . . . 13 (𝑞 = 𝑟 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑟)))
2322elrab 3631 . . . . . . . . . . . 12 (𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑟𝑋𝑐 ∈ (𝑁𝑟)))
24 simp-5l 784 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝜑)
25 simpr1l 1227 . . . . . . . . . . . . . . 15 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ ((𝑟𝑋𝑐 ∈ (𝑁𝑟)) ∧ 𝑏 ∈ (𝑁𝑟) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})) → 𝑟𝑋)
26253anassrs 1357 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑟𝑋)
27 simpr 488 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
28 simplr 768 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ∈ (𝑁𝑟))
29 sseq1 3943 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
30293anbi2d 1438 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
31 eleq1w 2875 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (𝑎 ∈ (𝑁𝑟) ↔ 𝑏 ∈ (𝑁𝑟)))
3230, 31anbi12d 633 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑏 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟))))
3332imbi1d 345 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → (((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
34 simpl1l 1221 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝜑)
359, 1, 10, 11, 12, 13, 14neiptoptop 21740 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ Top)
3635uniexd 7452 . . . . . . . . . . . . . . . . . . . 20 (𝜑 𝐽 ∈ V)
3715, 36eqeltrd 2893 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ V)
38 rabexg 5201 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ V → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V)
39 sseq2 3944 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑎𝑏𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
40 sseq1 3943 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏𝑋 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋))
4139, 403anbi23d 1436 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
4241anbi1d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
43 eleq1 2880 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏 ∈ (𝑁𝑟) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
4442, 43imbi12d 348 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
45 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑟 → (𝑝𝑋𝑟𝑋))
4645anbi2d 631 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → ((𝜑𝑝𝑋) ↔ (𝜑𝑟𝑋)))
47463anbi1d 1437 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋)))
48 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → (𝑁𝑝) = (𝑁𝑟))
4948eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑟)))
5047, 49anbi12d 633 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
5148eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑟)))
5250, 51imbi12d 348 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑟 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))))
5352, 10chvarvv 2005 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))
5444, 53vtoclg 3518 . . . . . . . . . . . . . . . . . . 19 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5537, 38, 543syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5634, 55mpcom 38 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
5733, 56chvarvv 2005 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
58573an1rs 1356 . . . . . . . . . . . . . . 15 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
5919, 58mpan2 690 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6024, 26, 27, 28, 59syl211anc 1373 . . . . . . . . . . . . 13 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
61 simplll 774 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝜑)
62 simprl 770 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑟𝑋)
63 simprr 772 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑐 ∈ (𝑁𝑟))
6448eleq2d 2878 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑟)))
6546, 64anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟))))
66 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = 𝑠 → (𝑁𝑞) = (𝑁𝑠))
6766eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = 𝑠 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑠)))
6867cbvralvw 3399 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
6968a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7048, 69rexeqbidv 3358 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7165, 70imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)) ↔ (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))))
72 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
7372anbi2d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ ((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))))
74 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑞)))
7574rexralbidv 3263 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)))
7673, 75imbi12d 348 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞)) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))))
7776, 13chvarvv 2005 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))
7871, 77chvarvv 2005 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
791ffvelrnda 6832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑟𝑋) → (𝑁𝑟) ∈ 𝒫 𝒫 𝑋)
8079elpwid 4511 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑟𝑋) → (𝑁𝑟) ⊆ 𝒫 𝑋)
8180sselda 3918 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏 ∈ 𝒫 𝑋)
8281elpwid 4511 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏𝑋)
8382sselda 3918 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → 𝑠𝑋)
8483a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → 𝑠𝑋))
8584ancrd 555 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8685ralimdva 3147 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → (∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8786reximdva 3236 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8887adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8978, 88mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9067elrab 3631 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9190ralbii 3136 . . . . . . . . . . . . . . . . 17 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9291rexbii 3213 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9389, 92sylibr 237 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
94 dfss3 3906 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9594biimpri 231 . . . . . . . . . . . . . . . 16 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9695reximi 3209 . . . . . . . . . . . . . . 15 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9793, 96syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9861, 62, 63, 97syl21anc 836 . . . . . . . . . . . . 13 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9960, 98r19.29a 3251 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10023, 99sylan2b 596 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ 𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
101100ralrimiva 3152 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10248eleq2d 2878 . . . . . . . . . . 11 (𝑝 = 𝑟 → ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
103102cbvralvw 3399 . . . . . . . . . 10 (∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
104101, 103sylibr 237 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝))
1059neipeltop 21738 . . . . . . . . 9 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ↔ ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝)))
10620, 104, 105sylanbrc 586 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽)
107 simpr 488 . . . . . . . . . 10 ((𝜑𝑝𝑋) → 𝑝𝑋)
108107anim1i 617 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
109 fveq2 6649 . . . . . . . . . . 11 (𝑞 = 𝑝 → (𝑁𝑞) = (𝑁𝑝))
110109eleq2d 2878 . . . . . . . . . 10 (𝑞 = 𝑝 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑝)))
111110elrab 3631 . . . . . . . . 9 (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
112108, 111sylibr 237 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
113 nfv 1915 . . . . . . . . 9 𝑞((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))
114 nfrab1 3340 . . . . . . . . 9 𝑞{𝑞𝑋𝑐 ∈ (𝑁𝑞)}
115 nfcv 2958 . . . . . . . . 9 𝑞𝑐
116 rabid 3334 . . . . . . . . . 10 (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑞𝑋𝑐 ∈ (𝑁𝑞)))
117 simplll 774 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝜑)
118 simprl 770 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑋)
119 simprr 772 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑐 ∈ (𝑁𝑞))
120 eleq1w 2875 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
121120anbi2d 631 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → ((𝜑𝑝𝑋) ↔ (𝜑𝑞𝑋)))
122 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
123122eleq2d 2878 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑞)))
124121, 123anbi12d 633 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞))))
125 elequ1 2119 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (𝑝𝑐𝑞𝑐))
126124, 125imbi12d 348 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐) ↔ (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)))
127 elequ2 2127 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → (𝑝𝑎𝑝𝑐))
12873, 127imbi12d 348 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑝𝑎) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)))
129128, 12chvarvv 2005 . . . . . . . . . . . . 13 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)
130126, 129chvarvv 2005 . . . . . . . . . . . 12 (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)
131117, 118, 119, 130syl21anc 836 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑐)
132131ex 416 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ((𝑞𝑋𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐))
133116, 132syl5bi 245 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑞𝑐))
134113, 114, 115, 133ssrd 3923 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)
135 eleq2 2881 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑝𝑑𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
136 sseq1 3943 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑑𝑐 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐))
137135, 136anbi12d 633 . . . . . . . . 9 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((𝑝𝑑𝑑𝑐) ↔ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)))
138137rspcev 3574 . . . . . . . 8 (({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
139106, 112, 134, 138syl12anc 835 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
14018, 139jca 515 . . . . . 6 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
141 nfv 1915 . . . . . . . 8 𝑑(𝜑𝑝𝑋)
142 nfv 1915 . . . . . . . . 9 𝑑 𝑐 𝐽
143 nfre1 3268 . . . . . . . . 9 𝑑𝑑𝐽 (𝑝𝑑𝑑𝑐)
144142, 143nfan 1900 . . . . . . . 8 𝑑(𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
145141, 144nfan 1900 . . . . . . 7 𝑑((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
146 simplll 774 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → (𝜑𝑝𝑋))
147 simpr 488 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑𝑐)
148 simpr1l 1227 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ ((𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)) ∧ 𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐)) → 𝑐 𝐽)
1491483anassrs 1357 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 𝐽)
150146, 16syl 17 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑋 = 𝐽)
151149, 150sseqtrrd 3959 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐𝑋)
152 simplr 768 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑 ∈ (𝑁𝑝))
153 sseq1 3943 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (𝑎𝑐𝑑𝑐))
1541533anbi2d 1438 . . . . . . . . . . 11 (𝑎 = 𝑑 → (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋)))
155 eleq1w 2875 . . . . . . . . . . 11 (𝑎 = 𝑑 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑑 ∈ (𝑁𝑝)))
156154, 155anbi12d 633 . . . . . . . . . 10 (𝑎 = 𝑑 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝))))
157156imbi1d 345 . . . . . . . . 9 (𝑎 = 𝑑 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
158 sseq2 3944 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑎𝑏𝑎𝑐))
159 sseq1 3943 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑏𝑋𝑐𝑋))
160158, 1593anbi23d 1436 . . . . . . . . . . . 12 (𝑏 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋)))
161160anbi1d 632 . . . . . . . . . . 11 (𝑏 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝))))
162 eleq1w 2875 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
163161, 162imbi12d 348 . . . . . . . . . 10 (𝑏 = 𝑐 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
164163, 10chvarvv 2005 . . . . . . . . 9 ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
165157, 164chvarvv 2005 . . . . . . . 8 ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
166146, 147, 151, 152, 165syl31anc 1370 . . . . . . 7 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 ∈ (𝑁𝑝))
1679neipeltop 21738 . . . . . . . . . . . . 13 (𝑑𝐽 ↔ (𝑑𝑋 ∧ ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝)))
168167simprbi 500 . . . . . . . . . . . 12 (𝑑𝐽 → ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝))
169168r19.21bi 3176 . . . . . . . . . . 11 ((𝑑𝐽𝑝𝑑) → 𝑑 ∈ (𝑁𝑝))
170169anim1i 617 . . . . . . . . . 10 (((𝑑𝐽𝑝𝑑) ∧ 𝑑𝑐) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
171170anasss 470 . . . . . . . . 9 ((𝑑𝐽 ∧ (𝑝𝑑𝑑𝑐)) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
172171reximi2 3210 . . . . . . . 8 (∃𝑑𝐽 (𝑝𝑑𝑑𝑐) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
173172ad2antll 728 . . . . . . 7 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
174145, 166, 173r19.29af 3292 . . . . . 6 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → 𝑐 ∈ (𝑁𝑝))
175140, 174impbida 800 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
176107, 16eleqtrd 2895 . . . . . 6 ((𝜑𝑝𝑋) → 𝑝 𝐽)
177 eqid 2801 . . . . . . 7 𝐽 = 𝐽
178177isneip 21714 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑝 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
17935, 176, 178syl2an2r 684 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
180175, 179bitr4d 285 . . . 4 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
181180eqrdv 2799 . . 3 ((𝜑𝑝𝑋) → (𝑁𝑝) = ((nei‘𝐽)‘{𝑝}))
182181mpteq2dva 5128 . 2 (𝜑 → (𝑝𝑋 ↦ (𝑁𝑝)) = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
1832, 182eqtrd 2836 1 (𝜑𝑁 = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wral 3109  wrex 3110  {crab 3113  Vcvv 3444  wss 3884  𝒫 cpw 4500  {csn 4528   cuni 4803  cmpt 5113  wf 6324  cfv 6328  ficfi 8862  Topctop 21502  neicnei 21706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-fin 8500  df-fi 8863  df-top 21503  df-nei 21707
This theorem is referenced by:  neiptopreu  21742  utopsnneiplem  22857
  Copyright terms: Public domain W3C validator