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

Theorem neiptopnei 20855
Description: Lemma for neiptopreu 20856. (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 6211 . 2 (𝜑𝑁 = (𝑝𝑋 ↦ (𝑁𝑝)))
31ffvelrnda 6320 . . . . . . . . . . . 12 ((𝜑𝑝𝑋) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
43adantr 481 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
54elpwid 4146 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ⊆ 𝒫 𝑋)
6 simpr 477 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
75, 6sseldd 3588 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ 𝒫 𝑋)
87elpwid 4146 . . . . . . . 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 20853 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1615adantr 481 . . . . . . . . 9 ((𝜑𝑝𝑋) → 𝑋 = 𝐽)
1716adantr 481 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑋 = 𝐽)
188, 17sseqtrd 3625 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 𝐽)
19 ssrab2 3671 . . . . . . . . . 10 {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋
2019a1i 11 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)
21 fveq2 6153 . . . . . . . . . . . . . 14 (𝑞 = 𝑟 → (𝑁𝑞) = (𝑁𝑟))
2221eleq2d 2684 . . . . . . . . . . . . 13 (𝑞 = 𝑟 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑟)))
2322elrab 3350 . . . . . . . . . . . 12 (𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑟𝑋𝑐 ∈ (𝑁𝑟)))
24 simp-5l 807 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝜑)
25 simpr1l 1116 . . . . . . . . . . . . . . 15 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ ((𝑟𝑋𝑐 ∈ (𝑁𝑟)) ∧ 𝑏 ∈ (𝑁𝑟) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})) → 𝑟𝑋)
26253anassrs 1287 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑟𝑋)
27 simpr 477 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
28 simplr 791 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ∈ (𝑁𝑟))
29 sseq1 3610 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
30293anbi2d 1401 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
31 eleq1 2686 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (𝑎 ∈ (𝑁𝑟) ↔ 𝑏 ∈ (𝑁𝑟)))
3230, 31anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑏 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟))))
3332imbi1d 331 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → (((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
34 simpl1l 1110 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝜑)
359, 1, 10, 11, 12, 13, 14neiptoptop 20854 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ Top)
36 uniexg 6915 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ Top → 𝐽 ∈ V)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 𝐽 ∈ V)
3815, 37eqeltrd 2698 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ V)
39 rabexg 4777 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ V → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V)
40 sseq2 3611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑎𝑏𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
41 sseq1 3610 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏𝑋 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋))
4240, 413anbi23d 1399 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
4342anbi1d 740 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
44 eleq1 2686 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏 ∈ (𝑁𝑟) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
4543, 44imbi12d 334 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
46 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑟 → (𝑝𝑋𝑟𝑋))
4746anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → ((𝜑𝑝𝑋) ↔ (𝜑𝑟𝑋)))
48473anbi1d 1400 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋)))
49 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → (𝑁𝑝) = (𝑁𝑟))
5049eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑟)))
5148, 50anbi12d 746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
5249eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑟)))
5351, 52imbi12d 334 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑟 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))))
5453, 10chvarv 2262 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))
5545, 54vtoclg 3255 . . . . . . . . . . . . . . . . . . 19 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5638, 39, 553syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5734, 56mpcom 38 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
5833, 57chvarv 2262 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
59583an1rs 1276 . . . . . . . . . . . . . . 15 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6019, 59mpan2 706 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6124, 26, 27, 28, 60syl211anc 1329 . . . . . . . . . . . . 13 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
62 simplll 797 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝜑)
63 simprl 793 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑟𝑋)
64 simprr 795 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑐 ∈ (𝑁𝑟))
6549eleq2d 2684 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑟)))
6647, 65anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟))))
67 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = 𝑠 → (𝑁𝑞) = (𝑁𝑠))
6867eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = 𝑠 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑠)))
6968cbvralv 3162 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
7069a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7149, 70rexeqbidv 3145 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7266, 71imbi12d 334 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)) ↔ (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))))
73 eleq1 2686 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
7473anbi2d 739 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ ((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))))
75 eleq1 2686 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑞)))
7675rexralbidv 3052 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)))
7774, 76imbi12d 334 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞)) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))))
7877, 13chvarv 2262 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))
7972, 78chvarv 2262 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
801ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑟𝑋) → (𝑁𝑟) ∈ 𝒫 𝒫 𝑋)
8180elpwid 4146 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑟𝑋) → (𝑁𝑟) ⊆ 𝒫 𝑋)
8281sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏 ∈ 𝒫 𝑋)
8382elpwid 4146 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏𝑋)
8483sselda 3587 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → 𝑠𝑋)
8584a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → 𝑠𝑋))
8685ancrd 576 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8786ralimdva 2957 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → (∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8887reximdva 3012 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8988adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
9079, 89mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9168elrab 3350 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9291ralbii 2975 . . . . . . . . . . . . . . . . 17 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9392rexbii 3035 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9490, 93sylibr 224 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
95 dfss3 3577 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9695biimpri 218 . . . . . . . . . . . . . . . 16 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9796reximi 3006 . . . . . . . . . . . . . . 15 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9894, 97syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9962, 63, 64, 98syl21anc 1322 . . . . . . . . . . . . 13 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
10061, 99r19.29a 3072 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10123, 100sylan2b 492 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ 𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
102101ralrimiva 2961 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10349eleq2d 2684 . . . . . . . . . . 11 (𝑝 = 𝑟 → ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
104103cbvralv 3162 . . . . . . . . . 10 (∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
105102, 104sylibr 224 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝))
1069neipeltop 20852 . . . . . . . . 9 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ↔ ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝)))
10720, 105, 106sylanbrc 697 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽)
108 simpr 477 . . . . . . . . . 10 ((𝜑𝑝𝑋) → 𝑝𝑋)
109108anim1i 591 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
110 fveq2 6153 . . . . . . . . . . 11 (𝑞 = 𝑝 → (𝑁𝑞) = (𝑁𝑝))
111110eleq2d 2684 . . . . . . . . . 10 (𝑞 = 𝑝 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑝)))
112111elrab 3350 . . . . . . . . 9 (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
113109, 112sylibr 224 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
114 nfv 1840 . . . . . . . . 9 𝑞((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))
115 nfrab1 3114 . . . . . . . . 9 𝑞{𝑞𝑋𝑐 ∈ (𝑁𝑞)}
116 nfcv 2761 . . . . . . . . 9 𝑞𝑐
117 rabid 3109 . . . . . . . . . 10 (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑞𝑋𝑐 ∈ (𝑁𝑞)))
118 simplll 797 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝜑)
119 simprl 793 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑋)
120 simprr 795 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑐 ∈ (𝑁𝑞))
121 eleq1 2686 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
122121anbi2d 739 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → ((𝜑𝑝𝑋) ↔ (𝜑𝑞𝑋)))
123 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
124123eleq2d 2684 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑞)))
125122, 124anbi12d 746 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞))))
126 elequ1 1994 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (𝑝𝑐𝑞𝑐))
127125, 126imbi12d 334 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐) ↔ (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)))
128 elequ2 2001 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → (𝑝𝑎𝑝𝑐))
12974, 128imbi12d 334 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑝𝑎) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)))
130129, 12chvarv 2262 . . . . . . . . . . . . 13 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)
131127, 130chvarv 2262 . . . . . . . . . . . 12 (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)
132118, 119, 120, 131syl21anc 1322 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑐)
133132ex 450 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ((𝑞𝑋𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐))
134117, 133syl5bi 232 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑞𝑐))
135114, 115, 116, 134ssrd 3592 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)
136 eleq2 2687 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑝𝑑𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
137 sseq1 3610 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑑𝑐 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐))
138136, 137anbi12d 746 . . . . . . . . 9 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((𝑝𝑑𝑑𝑐) ↔ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)))
139138rspcev 3298 . . . . . . . 8 (({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
140107, 113, 135, 139syl12anc 1321 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
14118, 140jca 554 . . . . . 6 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
142 nfv 1840 . . . . . . . 8 𝑑(𝜑𝑝𝑋)
143 nfv 1840 . . . . . . . . 9 𝑑 𝑐 𝐽
144 nfre1 3000 . . . . . . . . 9 𝑑𝑑𝐽 (𝑝𝑑𝑑𝑐)
145143, 144nfan 1825 . . . . . . . 8 𝑑(𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
146142, 145nfan 1825 . . . . . . 7 𝑑((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
147 simplll 797 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → (𝜑𝑝𝑋))
148 simpr 477 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑𝑐)
149 simpr1l 1116 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ ((𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)) ∧ 𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐)) → 𝑐 𝐽)
1501493anassrs 1287 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 𝐽)
151147, 16syl 17 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑋 = 𝐽)
152150, 151sseqtr4d 3626 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐𝑋)
153 simplr 791 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑 ∈ (𝑁𝑝))
154 sseq1 3610 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (𝑎𝑐𝑑𝑐))
1551543anbi2d 1401 . . . . . . . . . . 11 (𝑎 = 𝑑 → (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋)))
156 eleq1 2686 . . . . . . . . . . 11 (𝑎 = 𝑑 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑑 ∈ (𝑁𝑝)))
157155, 156anbi12d 746 . . . . . . . . . 10 (𝑎 = 𝑑 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝))))
158157imbi1d 331 . . . . . . . . 9 (𝑎 = 𝑑 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
159 sseq2 3611 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑎𝑏𝑎𝑐))
160 sseq1 3610 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑏𝑋𝑐𝑋))
161159, 1603anbi23d 1399 . . . . . . . . . . . 12 (𝑏 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋)))
162161anbi1d 740 . . . . . . . . . . 11 (𝑏 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝))))
163 eleq1 2686 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
164162, 163imbi12d 334 . . . . . . . . . 10 (𝑏 = 𝑐 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
165164, 10chvarv 2262 . . . . . . . . 9 ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
166158, 165chvarv 2262 . . . . . . . 8 ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
167147, 148, 152, 153, 166syl31anc 1326 . . . . . . 7 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 ∈ (𝑁𝑝))
1689neipeltop 20852 . . . . . . . . . . . . 13 (𝑑𝐽 ↔ (𝑑𝑋 ∧ ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝)))
169168simprbi 480 . . . . . . . . . . . 12 (𝑑𝐽 → ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝))
170169r19.21bi 2927 . . . . . . . . . . 11 ((𝑑𝐽𝑝𝑑) → 𝑑 ∈ (𝑁𝑝))
171170anim1i 591 . . . . . . . . . 10 (((𝑑𝐽𝑝𝑑) ∧ 𝑑𝑐) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
172171anasss 678 . . . . . . . . 9 ((𝑑𝐽 ∧ (𝑝𝑑𝑑𝑐)) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
173172reximi2 3005 . . . . . . . 8 (∃𝑑𝐽 (𝑝𝑑𝑑𝑐) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
174173ad2antll 764 . . . . . . 7 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
175146, 167, 174r19.29af 3070 . . . . . 6 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → 𝑐 ∈ (𝑁𝑝))
176141, 175impbida 876 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
17735adantr 481 . . . . . 6 ((𝜑𝑝𝑋) → 𝐽 ∈ Top)
178108, 16eleqtrd 2700 . . . . . 6 ((𝜑𝑝𝑋) → 𝑝 𝐽)
179 eqid 2621 . . . . . . 7 𝐽 = 𝐽
180179isneip 20828 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑝 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
181177, 178, 180syl2anc 692 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
182176, 181bitr4d 271 . . . 4 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
183182eqrdv 2619 . . 3 ((𝜑𝑝𝑋) → (𝑁𝑝) = ((nei‘𝐽)‘{𝑝}))
184183mpteq2dva 4709 . 2 (𝜑 → (𝑝𝑋 ↦ (𝑁𝑝)) = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
1852, 184eqtrd 2655 1 (𝜑𝑁 = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  wss 3559  𝒫 cpw 4135  {csn 4153   cuni 4407  cmpt 4678  wf 5848  cfv 5852  ficfi 8267  Topctop 20626  neicnei 20820
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-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7907  df-fin 7910  df-fi 8268  df-top 20627  df-nei 20821
This theorem is referenced by:  neiptopreu  20856  utopsnneiplem  21970
  Copyright terms: Public domain W3C validator