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

Theorem neiptopnei 21157
Description: Lemma for neiptopreu 21158. (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 6391 . 2 (𝜑𝑁 = (𝑝𝑋 ↦ (𝑁𝑝)))
31ffvelrnda 6502 . . . . . . . . . . . 12 ((𝜑𝑝𝑋) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
43adantr 466 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
54elpwid 4309 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ⊆ 𝒫 𝑋)
6 simpr 471 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
75, 6sseldd 3753 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ 𝒫 𝑋)
87elpwid 4309 . . . . . . . 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 21155 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1615adantr 466 . . . . . . . . 9 ((𝜑𝑝𝑋) → 𝑋 = 𝐽)
1716adantr 466 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑋 = 𝐽)
188, 17sseqtrd 3790 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 𝐽)
19 ssrab2 3836 . . . . . . . . . 10 {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋
2019a1i 11 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)
21 fveq2 6332 . . . . . . . . . . . . . 14 (𝑞 = 𝑟 → (𝑁𝑞) = (𝑁𝑟))
2221eleq2d 2836 . . . . . . . . . . . . 13 (𝑞 = 𝑟 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑟)))
2322elrab 3515 . . . . . . . . . . . 12 (𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑟𝑋𝑐 ∈ (𝑁𝑟)))
24 simp-5l 772 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝜑)
25 simpr1l 1290 . . . . . . . . . . . . . . 15 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ ((𝑟𝑋𝑐 ∈ (𝑁𝑟)) ∧ 𝑏 ∈ (𝑁𝑟) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})) → 𝑟𝑋)
26253anassrs 1453 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑟𝑋)
27 simpr 471 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
28 simplr 752 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ∈ (𝑁𝑟))
29 sseq1 3775 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
30293anbi2d 1552 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
31 eleq1w 2833 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (𝑎 ∈ (𝑁𝑟) ↔ 𝑏 ∈ (𝑁𝑟)))
3230, 31anbi12d 616 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑏 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟))))
3332imbi1d 330 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → (((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
34 simpl1l 1278 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝜑)
359, 1, 10, 11, 12, 13, 14neiptoptop 21156 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ Top)
36 uniexg 7102 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ Top → 𝐽 ∈ V)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 𝐽 ∈ V)
3815, 37eqeltrd 2850 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ V)
39 rabexg 4945 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ V → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V)
40 sseq2 3776 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑎𝑏𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
41 sseq1 3775 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏𝑋 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋))
4240, 413anbi23d 1550 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
4342anbi1d 615 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
44 eleq1 2838 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏 ∈ (𝑁𝑟) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
4543, 44imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
46 eleq1w 2833 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑟 → (𝑝𝑋𝑟𝑋))
4746anbi2d 614 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → ((𝜑𝑝𝑋) ↔ (𝜑𝑟𝑋)))
48473anbi1d 1551 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋)))
49 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → (𝑁𝑝) = (𝑁𝑟))
5049eleq2d 2836 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑟)))
5148, 50anbi12d 616 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
5249eleq2d 2836 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑟)))
5351, 52imbi12d 333 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑟 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))))
5453, 10chvarv 2425 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))
5545, 54vtoclg 3417 . . . . . . . . . . . . . . . . . . 19 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5638, 39, 553syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5734, 56mpcom 38 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
5833, 57chvarv 2425 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
59583an1rs 1452 . . . . . . . . . . . . . . 15 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6019, 59mpan2 671 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6124, 26, 27, 28, 60syl211anc 1482 . . . . . . . . . . . . 13 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
62 simplll 758 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝜑)
63 simprl 754 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑟𝑋)
64 simprr 756 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑐 ∈ (𝑁𝑟))
6549eleq2d 2836 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑟)))
6647, 65anbi12d 616 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟))))
67 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = 𝑠 → (𝑁𝑞) = (𝑁𝑠))
6867eleq2d 2836 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = 𝑠 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑠)))
6968cbvralv 3320 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
7069a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7149, 70rexeqbidv 3302 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7266, 71imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)) ↔ (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))))
73 eleq1w 2833 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
7473anbi2d 614 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ ((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))))
75 eleq1w 2833 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑞)))
7675rexralbidv 3206 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)))
7774, 76imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞)) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))))
7877, 13chvarv 2425 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))
7972, 78chvarv 2425 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
801ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑟𝑋) → (𝑁𝑟) ∈ 𝒫 𝒫 𝑋)
8180elpwid 4309 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑟𝑋) → (𝑁𝑟) ⊆ 𝒫 𝑋)
8281sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏 ∈ 𝒫 𝑋)
8382elpwid 4309 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏𝑋)
8483sselda 3752 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → 𝑠𝑋)
8584a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → 𝑠𝑋))
8685ancrd 541 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8786ralimdva 3111 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → (∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8887reximdva 3165 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8988adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
9079, 89mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9168elrab 3515 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9291ralbii 3129 . . . . . . . . . . . . . . . . 17 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9392rexbii 3189 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9490, 93sylibr 224 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
95 dfss3 3741 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9695biimpri 218 . . . . . . . . . . . . . . . 16 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9796reximi 3159 . . . . . . . . . . . . . . 15 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9894, 97syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9962, 63, 64, 98syl21anc 1475 . . . . . . . . . . . . 13 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
10061, 99r19.29a 3226 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10123, 100sylan2b 581 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ 𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
102101ralrimiva 3115 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10349eleq2d 2836 . . . . . . . . . . 11 (𝑝 = 𝑟 → ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
104103cbvralv 3320 . . . . . . . . . 10 (∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
105102, 104sylibr 224 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝))
1069neipeltop 21154 . . . . . . . . 9 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ↔ ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝)))
10720, 105, 106sylanbrc 572 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽)
108 simpr 471 . . . . . . . . . 10 ((𝜑𝑝𝑋) → 𝑝𝑋)
109108anim1i 602 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
110 fveq2 6332 . . . . . . . . . . 11 (𝑞 = 𝑝 → (𝑁𝑞) = (𝑁𝑝))
111110eleq2d 2836 . . . . . . . . . 10 (𝑞 = 𝑝 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑝)))
112111elrab 3515 . . . . . . . . 9 (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
113109, 112sylibr 224 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
114 nfv 1995 . . . . . . . . 9 𝑞((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))
115 nfrab1 3271 . . . . . . . . 9 𝑞{𝑞𝑋𝑐 ∈ (𝑁𝑞)}
116 nfcv 2913 . . . . . . . . 9 𝑞𝑐
117 rabid 3264 . . . . . . . . . 10 (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑞𝑋𝑐 ∈ (𝑁𝑞)))
118 simplll 758 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝜑)
119 simprl 754 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑋)
120 simprr 756 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑐 ∈ (𝑁𝑞))
121 eleq1w 2833 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
122121anbi2d 614 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → ((𝜑𝑝𝑋) ↔ (𝜑𝑞𝑋)))
123 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
124123eleq2d 2836 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑞)))
125122, 124anbi12d 616 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞))))
126 elequ1 2152 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (𝑝𝑐𝑞𝑐))
127125, 126imbi12d 333 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐) ↔ (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)))
128 elequ2 2159 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → (𝑝𝑎𝑝𝑐))
12974, 128imbi12d 333 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑝𝑎) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)))
130129, 12chvarv 2425 . . . . . . . . . . . . 13 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)
131127, 130chvarv 2425 . . . . . . . . . . . 12 (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)
132118, 119, 120, 131syl21anc 1475 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑐)
133132ex 397 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ((𝑞𝑋𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐))
134117, 133syl5bi 232 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑞𝑐))
135114, 115, 116, 134ssrd 3757 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)
136 eleq2 2839 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑝𝑑𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
137 sseq1 3775 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑑𝑐 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐))
138136, 137anbi12d 616 . . . . . . . . 9 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((𝑝𝑑𝑑𝑐) ↔ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)))
139138rspcev 3460 . . . . . . . 8 (({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
140107, 113, 135, 139syl12anc 1474 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
14118, 140jca 501 . . . . . 6 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
142 nfv 1995 . . . . . . . 8 𝑑(𝜑𝑝𝑋)
143 nfv 1995 . . . . . . . . 9 𝑑 𝑐 𝐽
144 nfre1 3153 . . . . . . . . 9 𝑑𝑑𝐽 (𝑝𝑑𝑑𝑐)
145143, 144nfan 1980 . . . . . . . 8 𝑑(𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
146142, 145nfan 1980 . . . . . . 7 𝑑((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
147 simplll 758 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → (𝜑𝑝𝑋))
148 simpr 471 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑𝑐)
149 simpr1l 1290 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ ((𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)) ∧ 𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐)) → 𝑐 𝐽)
1501493anassrs 1453 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 𝐽)
151147, 16syl 17 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑋 = 𝐽)
152150, 151sseqtr4d 3791 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐𝑋)
153 simplr 752 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑 ∈ (𝑁𝑝))
154 sseq1 3775 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (𝑎𝑐𝑑𝑐))
1551543anbi2d 1552 . . . . . . . . . . 11 (𝑎 = 𝑑 → (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋)))
156 eleq1w 2833 . . . . . . . . . . 11 (𝑎 = 𝑑 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑑 ∈ (𝑁𝑝)))
157155, 156anbi12d 616 . . . . . . . . . 10 (𝑎 = 𝑑 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝))))
158157imbi1d 330 . . . . . . . . 9 (𝑎 = 𝑑 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
159 sseq2 3776 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑎𝑏𝑎𝑐))
160 sseq1 3775 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑏𝑋𝑐𝑋))
161159, 1603anbi23d 1550 . . . . . . . . . . . 12 (𝑏 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋)))
162161anbi1d 615 . . . . . . . . . . 11 (𝑏 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝))))
163 eleq1w 2833 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
164162, 163imbi12d 333 . . . . . . . . . 10 (𝑏 = 𝑐 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
165164, 10chvarv 2425 . . . . . . . . 9 ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
166158, 165chvarv 2425 . . . . . . . 8 ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
167147, 148, 152, 153, 166syl31anc 1479 . . . . . . 7 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 ∈ (𝑁𝑝))
1689neipeltop 21154 . . . . . . . . . . . . 13 (𝑑𝐽 ↔ (𝑑𝑋 ∧ ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝)))
169168simprbi 484 . . . . . . . . . . . 12 (𝑑𝐽 → ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝))
170169r19.21bi 3081 . . . . . . . . . . 11 ((𝑑𝐽𝑝𝑑) → 𝑑 ∈ (𝑁𝑝))
171170anim1i 602 . . . . . . . . . 10 (((𝑑𝐽𝑝𝑑) ∧ 𝑑𝑐) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
172171anasss 457 . . . . . . . . 9 ((𝑑𝐽 ∧ (𝑝𝑑𝑑𝑐)) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
173172reximi2 3158 . . . . . . . 8 (∃𝑑𝐽 (𝑝𝑑𝑑𝑐) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
174173ad2antll 708 . . . . . . 7 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
175146, 167, 174r19.29af 3224 . . . . . 6 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → 𝑐 ∈ (𝑁𝑝))
176141, 175impbida 802 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
17735adantr 466 . . . . . 6 ((𝜑𝑝𝑋) → 𝐽 ∈ Top)
178108, 16eleqtrd 2852 . . . . . 6 ((𝜑𝑝𝑋) → 𝑝 𝐽)
179 eqid 2771 . . . . . . 7 𝐽 = 𝐽
180179isneip 21130 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑝 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
181177, 178, 180syl2anc 573 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
182176, 181bitr4d 271 . . . 4 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
183182eqrdv 2769 . . 3 ((𝜑𝑝𝑋) → (𝑁𝑝) = ((nei‘𝐽)‘{𝑝}))
184183mpteq2dva 4878 . 2 (𝜑 → (𝑝𝑋 ↦ (𝑁𝑝)) = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
1852, 184eqtrd 2805 1 (𝜑𝑁 = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  wss 3723  𝒫 cpw 4297  {csn 4316   cuni 4574  cmpt 4863  wf 6027  cfv 6031  ficfi 8472  Topctop 20918  neicnei 21122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-fin 8113  df-fi 8473  df-top 20919  df-nei 21123
This theorem is referenced by:  neiptopreu  21158  utopsnneiplem  22271
  Copyright terms: Public domain W3C validator