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

Theorem neiptopnei 21154
Description: Lemma for neiptopreu 21155. (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 6473 . 2 (𝜑𝑁 = (𝑝𝑋 ↦ (𝑁𝑝)))
31ffvelrnda 6584 . . . . . . . . . . . 12 ((𝜑𝑝𝑋) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
43adantr 468 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
54elpwid 4370 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ⊆ 𝒫 𝑋)
6 simpr 473 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
75, 6sseldd 3806 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ 𝒫 𝑋)
87elpwid 4370 . . . . . . . 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 21152 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1615adantr 468 . . . . . . . . 9 ((𝜑𝑝𝑋) → 𝑋 = 𝐽)
1716adantr 468 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑋 = 𝐽)
188, 17sseqtrd 3845 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 𝐽)
19 ssrab2 3891 . . . . . . . . . 10 {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋
2019a1i 11 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)
21 fveq2 6411 . . . . . . . . . . . . . 14 (𝑞 = 𝑟 → (𝑁𝑞) = (𝑁𝑟))
2221eleq2d 2878 . . . . . . . . . . . . 13 (𝑞 = 𝑟 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑟)))
2322elrab 3566 . . . . . . . . . . . 12 (𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑟𝑋𝑐 ∈ (𝑁𝑟)))
24 simp-5l 796 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝜑)
25 simpr1l 1298 . . . . . . . . . . . . . . 15 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ ((𝑟𝑋𝑐 ∈ (𝑁𝑟)) ∧ 𝑏 ∈ (𝑁𝑟) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})) → 𝑟𝑋)
26253anassrs 1462 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑟𝑋)
27 simpr 473 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
28 simplr 776 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ∈ (𝑁𝑟))
29 sseq1 3830 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
30293anbi2d 1558 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
31 eleq1w 2875 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (𝑎 ∈ (𝑁𝑟) ↔ 𝑏 ∈ (𝑁𝑟)))
3230, 31anbi12d 618 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑏 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟))))
3332imbi1d 332 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → (((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
34 simpl1l 1286 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝜑)
359, 1, 10, 11, 12, 13, 14neiptoptop 21153 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ Top)
36 uniexg 7188 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ Top → 𝐽 ∈ V)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 𝐽 ∈ V)
3815, 37eqeltrd 2892 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ V)
39 rabexg 5013 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ V → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V)
40 sseq2 3831 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑎𝑏𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
41 sseq1 3830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏𝑋 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋))
4240, 413anbi23d 1556 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
4342anbi1d 617 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
44 eleq1 2880 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏 ∈ (𝑁𝑟) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
4543, 44imbi12d 335 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
46 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑟 → (𝑝𝑋𝑟𝑋))
4746anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → ((𝜑𝑝𝑋) ↔ (𝜑𝑟𝑋)))
48473anbi1d 1557 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋)))
49 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → (𝑁𝑝) = (𝑁𝑟))
5049eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑟)))
5148, 50anbi12d 618 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
5249eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑟)))
5351, 52imbi12d 335 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑟 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))))
5453, 10chvarv 2439 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))
5545, 54vtoclg 3466 . . . . . . . . . . . . . . . . . . 19 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5638, 39, 553syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5734, 56mpcom 38 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
5833, 57chvarv 2439 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
59583an1rs 1461 . . . . . . . . . . . . . . 15 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6019, 59mpan2 674 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6124, 26, 27, 28, 60syl211anc 1488 . . . . . . . . . . . . 13 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
62 simplll 782 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝜑)
63 simprl 778 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑟𝑋)
64 simprr 780 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑐 ∈ (𝑁𝑟))
6549eleq2d 2878 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑟)))
6647, 65anbi12d 618 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟))))
67 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = 𝑠 → (𝑁𝑞) = (𝑁𝑠))
6867eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = 𝑠 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑠)))
6968cbvralv 3367 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
7069a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7149, 70rexeqbidv 3349 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7266, 71imbi12d 335 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)) ↔ (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))))
73 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
7473anbi2d 616 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ ((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))))
75 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑞)))
7675rexralbidv 3253 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)))
7774, 76imbi12d 335 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞)) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))))
7877, 13chvarv 2439 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))
7972, 78chvarv 2439 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
801ffvelrnda 6584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑟𝑋) → (𝑁𝑟) ∈ 𝒫 𝒫 𝑋)
8180elpwid 4370 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑟𝑋) → (𝑁𝑟) ⊆ 𝒫 𝑋)
8281sselda 3805 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏 ∈ 𝒫 𝑋)
8382elpwid 4370 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏𝑋)
8483sselda 3805 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → 𝑠𝑋)
8584a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → 𝑠𝑋))
8685ancrd 543 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8786ralimdva 3157 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → (∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8887reximdva 3211 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8988adantr 468 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
9079, 89mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9168elrab 3566 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9291ralbii 3175 . . . . . . . . . . . . . . . . 17 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9392rexbii 3236 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9490, 93sylibr 225 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
95 dfss3 3794 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9695biimpri 219 . . . . . . . . . . . . . . . 16 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9796reximi 3205 . . . . . . . . . . . . . . 15 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9894, 97syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9962, 63, 64, 98syl21anc 857 . . . . . . . . . . . . 13 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
10061, 99r19.29a 3273 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10123, 100sylan2b 583 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ 𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
102101ralrimiva 3161 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10349eleq2d 2878 . . . . . . . . . . 11 (𝑝 = 𝑟 → ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
104103cbvralv 3367 . . . . . . . . . 10 (∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
105102, 104sylibr 225 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝))
1069neipeltop 21151 . . . . . . . . 9 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ↔ ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝)))
10720, 105, 106sylanbrc 574 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽)
108 simpr 473 . . . . . . . . . 10 ((𝜑𝑝𝑋) → 𝑝𝑋)
109108anim1i 604 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
110 fveq2 6411 . . . . . . . . . . 11 (𝑞 = 𝑝 → (𝑁𝑞) = (𝑁𝑝))
111110eleq2d 2878 . . . . . . . . . 10 (𝑞 = 𝑝 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑝)))
112111elrab 3566 . . . . . . . . 9 (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
113109, 112sylibr 225 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
114 nfv 2005 . . . . . . . . 9 𝑞((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))
115 nfrab1 3318 . . . . . . . . 9 𝑞{𝑞𝑋𝑐 ∈ (𝑁𝑞)}
116 nfcv 2955 . . . . . . . . 9 𝑞𝑐
117 rabid 3311 . . . . . . . . . 10 (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑞𝑋𝑐 ∈ (𝑁𝑞)))
118 simplll 782 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝜑)
119 simprl 778 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑋)
120 simprr 780 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑐 ∈ (𝑁𝑞))
121 eleq1w 2875 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
122121anbi2d 616 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → ((𝜑𝑝𝑋) ↔ (𝜑𝑞𝑋)))
123 fveq2 6411 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
124123eleq2d 2878 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑞)))
125122, 124anbi12d 618 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞))))
126 elequ1 2164 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (𝑝𝑐𝑞𝑐))
127125, 126imbi12d 335 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐) ↔ (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)))
128 elequ2 2171 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → (𝑝𝑎𝑝𝑐))
12974, 128imbi12d 335 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑝𝑎) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)))
130129, 12chvarv 2439 . . . . . . . . . . . . 13 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)
131127, 130chvarv 2439 . . . . . . . . . . . 12 (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)
132118, 119, 120, 131syl21anc 857 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑐)
133132ex 399 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ((𝑞𝑋𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐))
134117, 133syl5bi 233 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑞𝑐))
135114, 115, 116, 134ssrd 3810 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)
136 eleq2 2881 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑝𝑑𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
137 sseq1 3830 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑑𝑐 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐))
138136, 137anbi12d 618 . . . . . . . . 9 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((𝑝𝑑𝑑𝑐) ↔ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)))
139138rspcev 3509 . . . . . . . 8 (({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
140107, 113, 135, 139syl12anc 856 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
14118, 140jca 503 . . . . . 6 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
142 nfv 2005 . . . . . . . 8 𝑑(𝜑𝑝𝑋)
143 nfv 2005 . . . . . . . . 9 𝑑 𝑐 𝐽
144 nfre1 3199 . . . . . . . . 9 𝑑𝑑𝐽 (𝑝𝑑𝑑𝑐)
145143, 144nfan 1990 . . . . . . . 8 𝑑(𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
146142, 145nfan 1990 . . . . . . 7 𝑑((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
147 simplll 782 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → (𝜑𝑝𝑋))
148 simpr 473 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑𝑐)
149 simpr1l 1298 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ ((𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)) ∧ 𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐)) → 𝑐 𝐽)
1501493anassrs 1462 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 𝐽)
151147, 16syl 17 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑋 = 𝐽)
152150, 151sseqtr4d 3846 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐𝑋)
153 simplr 776 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑 ∈ (𝑁𝑝))
154 sseq1 3830 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (𝑎𝑐𝑑𝑐))
1551543anbi2d 1558 . . . . . . . . . . 11 (𝑎 = 𝑑 → (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋)))
156 eleq1w 2875 . . . . . . . . . . 11 (𝑎 = 𝑑 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑑 ∈ (𝑁𝑝)))
157155, 156anbi12d 618 . . . . . . . . . 10 (𝑎 = 𝑑 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝))))
158157imbi1d 332 . . . . . . . . 9 (𝑎 = 𝑑 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
159 sseq2 3831 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑎𝑏𝑎𝑐))
160 sseq1 3830 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑏𝑋𝑐𝑋))
161159, 1603anbi23d 1556 . . . . . . . . . . . 12 (𝑏 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋)))
162161anbi1d 617 . . . . . . . . . . 11 (𝑏 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝))))
163 eleq1w 2875 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
164162, 163imbi12d 335 . . . . . . . . . 10 (𝑏 = 𝑐 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
165164, 10chvarv 2439 . . . . . . . . 9 ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
166158, 165chvarv 2439 . . . . . . . 8 ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
167147, 148, 152, 153, 166syl31anc 1485 . . . . . . 7 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 ∈ (𝑁𝑝))
1689neipeltop 21151 . . . . . . . . . . . . 13 (𝑑𝐽 ↔ (𝑑𝑋 ∧ ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝)))
169168simprbi 486 . . . . . . . . . . . 12 (𝑑𝐽 → ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝))
170169r19.21bi 3127 . . . . . . . . . . 11 ((𝑑𝐽𝑝𝑑) → 𝑑 ∈ (𝑁𝑝))
171170anim1i 604 . . . . . . . . . 10 (((𝑑𝐽𝑝𝑑) ∧ 𝑑𝑐) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
172171anasss 454 . . . . . . . . 9 ((𝑑𝐽 ∧ (𝑝𝑑𝑑𝑐)) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
173172reximi2 3204 . . . . . . . 8 (∃𝑑𝐽 (𝑝𝑑𝑑𝑐) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
174173ad2antll 711 . . . . . . 7 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
175146, 167, 174r19.29af 3271 . . . . . 6 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → 𝑐 ∈ (𝑁𝑝))
176141, 175impbida 826 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
17735adantr 468 . . . . . 6 ((𝜑𝑝𝑋) → 𝐽 ∈ Top)
178108, 16eleqtrd 2894 . . . . . 6 ((𝜑𝑝𝑋) → 𝑝 𝐽)
179 eqid 2813 . . . . . . 7 𝐽 = 𝐽
180179isneip 21127 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑝 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
181177, 178, 180syl2anc 575 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
182176, 181bitr4d 273 . . . 4 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
183182eqrdv 2811 . . 3 ((𝜑𝑝𝑋) → (𝑁𝑝) = ((nei‘𝐽)‘{𝑝}))
184183mpteq2dva 4945 . 2 (𝜑 → (𝑝𝑋 ↦ (𝑁𝑝)) = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
1852, 184eqtrd 2847 1 (𝜑𝑁 = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  wral 3103  wrex 3104  {crab 3107  Vcvv 3398  wss 3776  𝒫 cpw 4358  {csn 4377   cuni 4637  cmpt 4930  wf 6100  cfv 6104  ficfi 8558  Topctop 20915  neicnei 21119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-oadd 7803  df-er 7982  df-en 8196  df-fin 8199  df-fi 8559  df-top 20916  df-nei 21120
This theorem is referenced by:  neiptopreu  21155  utopsnneiplem  22268
  Copyright terms: Public domain W3C validator