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

Theorem neiptopnei 20746
Description: Lemma for neiptopreu 20747. (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 6159 . 2 (𝜑𝑁 = (𝑝𝑋 ↦ (𝑁𝑝)))
31ffvelrnda 6267 . . . . . . . . . . . 12 ((𝜑𝑝𝑋) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
43adantr 480 . . . . . . . . . . 11 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ∈ 𝒫 𝒫 𝑋)
54elpwid 4118 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑁𝑝) ⊆ 𝒫 𝑋)
6 simpr 476 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
75, 6sseldd 3569 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 ∈ 𝒫 𝑋)
87elpwid 4118 . . . . . . . 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 20744 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1615adantr 480 . . . . . . . . 9 ((𝜑𝑝𝑋) → 𝑋 = 𝐽)
1716adantr 480 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑋 = 𝐽)
188, 17sseqtrd 3604 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑐 𝐽)
19 ssrab2 3650 . . . . . . . . . 10 {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋
2019a1i 11 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)
21 fveq2 6103 . . . . . . . . . . . . . 14 (𝑞 = 𝑟 → (𝑁𝑞) = (𝑁𝑟))
2221eleq2d 2673 . . . . . . . . . . . . 13 (𝑞 = 𝑟 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑟)))
2322elrab 3331 . . . . . . . . . . . 12 (𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑟𝑋𝑐 ∈ (𝑁𝑟)))
24 simp-5l 804 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝜑)
25 simpr1l 1111 . . . . . . . . . . . . . . 15 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ ((𝑟𝑋𝑐 ∈ (𝑁𝑟)) ∧ 𝑏 ∈ (𝑁𝑟) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})) → 𝑟𝑋)
26253anassrs 1282 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑟𝑋)
27 simpr 476 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
28 simplr 788 . . . . . . . . . . . . . 14 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → 𝑏 ∈ (𝑁𝑟))
29 sseq1 3589 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → (𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
30293anbi2d 1396 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
31 eleq1 2676 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → (𝑎 ∈ (𝑁𝑟) ↔ 𝑏 ∈ (𝑁𝑟)))
3230, 31anbi12d 743 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑏 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟))))
3332imbi1d 330 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → (((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
34 simpl1l 1105 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝜑)
359, 1, 10, 11, 12, 13, 14neiptoptop 20745 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ Top)
36 uniexg 6853 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ Top → 𝐽 ∈ V)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 𝐽 ∈ V)
3815, 37eqeltrd 2688 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ V)
39 rabexg 4739 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ V → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V)
40 sseq2 3590 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑎𝑏𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
41 sseq1 3589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏𝑋 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋))
4240, 413anbi23d 1394 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋)))
4342anbi1d 737 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
44 eleq1 2676 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑏 ∈ (𝑁𝑟) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
4543, 44imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))))
46 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑟 → (𝑝𝑋𝑟𝑋))
4746anbi2d 736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → ((𝜑𝑝𝑋) ↔ (𝜑𝑟𝑋)))
48473anbi1d 1395 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋)))
49 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑟 → (𝑁𝑝) = (𝑁𝑟))
5049eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = 𝑟 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑟)))
5148, 50anbi12d 743 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟))))
5249eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = 𝑟 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑟)))
5351, 52imbi12d 333 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑟 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))))
5453, 10chvarv 2251 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → 𝑏 ∈ (𝑁𝑟))
5545, 54vtoclg 3239 . . . . . . . . . . . . . . . . . . 19 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ V → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5638, 39, 553syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
5734, 56mpcom 37 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟𝑋) ∧ 𝑎 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
5833, 57chvarv 2251 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
59583an1rs 1271 . . . . . . . . . . . . . . 15 ((((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6019, 59mpan2 703 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ 𝑏 ∈ (𝑁𝑟)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
6124, 26, 27, 28, 60syl211anc 1324 . . . . . . . . . . . . 13 ((((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
62 simplll 794 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝜑)
63 simprl 790 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑟𝑋)
64 simprr 792 . . . . . . . . . . . . . 14 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → 𝑐 ∈ (𝑁𝑟))
6549eleq2d 2673 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑟)))
6647, 65anbi12d 743 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟))))
67 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 = 𝑠 → (𝑁𝑞) = (𝑁𝑠))
6867eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 = 𝑠 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑠)))
6968cbvralv 3147 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
7069a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑟 → (∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7149, 70rexeqbidv 3130 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑟 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠)))
7266, 71imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑟 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)) ↔ (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))))
73 eleq1 2676 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
7473anbi2d 736 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ ((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))))
75 eleq1 2676 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑐 → (𝑎 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑞)))
7675rexralbidv 3040 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞)))
7774, 76imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞)) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))))
7877, 13chvarv 2251 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑐 ∈ (𝑁𝑞))
7972, 78chvarv 2251 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠))
801ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑟𝑋) → (𝑁𝑟) ∈ 𝒫 𝒫 𝑋)
8180elpwid 4118 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑟𝑋) → (𝑁𝑟) ⊆ 𝒫 𝑋)
8281sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏 ∈ 𝒫 𝑋)
8382elpwid 4118 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → 𝑏𝑋)
8483sselda 3568 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → 𝑠𝑋)
8584a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → 𝑠𝑋))
8685ancrd 575 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) ∧ 𝑠𝑏) → (𝑐 ∈ (𝑁𝑠) → (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8786ralimdva 2945 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑏 ∈ (𝑁𝑟)) → (∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8887reximdva 3000 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
8988adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑐 ∈ (𝑁𝑠) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠))))
9079, 89mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9168elrab 3331 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9291ralbii 2963 . . . . . . . . . . . . . . . . 17 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9392rexbii 3023 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 (𝑠𝑋𝑐 ∈ (𝑁𝑠)))
9490, 93sylibr 223 . . . . . . . . . . . . . . 15 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
95 dfss3 3558 . . . . . . . . . . . . . . . . 17 (𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ ∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9695biimpri 217 . . . . . . . . . . . . . . . 16 (∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9796reximi 2994 . . . . . . . . . . . . . . 15 (∃𝑏 ∈ (𝑁𝑟)∀𝑠𝑏 𝑠 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9894, 97syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑟𝑋) ∧ 𝑐 ∈ (𝑁𝑟)) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
9962, 63, 64, 98syl21anc 1317 . . . . . . . . . . . . 13 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → ∃𝑏 ∈ (𝑁𝑟)𝑏 ⊆ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
10061, 99r19.29a 3060 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑟𝑋𝑐 ∈ (𝑁𝑟))) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10123, 100sylan2b 491 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ 𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
102101ralrimiva 2949 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
10349eleq2d 2673 . . . . . . . . . . 11 (𝑝 = 𝑟 → ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟)))
104103cbvralv 3147 . . . . . . . . . 10 (∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝) ↔ ∀𝑟 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑟))
105102, 104sylibr 223 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝))
1069neipeltop 20743 . . . . . . . . 9 ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ↔ ({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑋 ∧ ∀𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ (𝑁𝑝)))
10720, 105, 106sylanbrc 695 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽)
108 simpr 476 . . . . . . . . . 10 ((𝜑𝑝𝑋) → 𝑝𝑋)
109108anim1i 590 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
110 fveq2 6103 . . . . . . . . . . 11 (𝑞 = 𝑝 → (𝑁𝑞) = (𝑁𝑝))
111110eleq2d 2673 . . . . . . . . . 10 (𝑞 = 𝑝 → (𝑐 ∈ (𝑁𝑞) ↔ 𝑐 ∈ (𝑁𝑝)))
112111elrab 3331 . . . . . . . . 9 (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑝𝑋𝑐 ∈ (𝑁𝑝)))
113109, 112sylibr 223 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)})
114 nfv 1830 . . . . . . . . 9 𝑞((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝))
115 nfrab1 3099 . . . . . . . . 9 𝑞{𝑞𝑋𝑐 ∈ (𝑁𝑞)}
116 nfcv 2751 . . . . . . . . 9 𝑞𝑐
117 rabid 3095 . . . . . . . . . 10 (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ↔ (𝑞𝑋𝑐 ∈ (𝑁𝑞)))
118 simplll 794 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝜑)
119 simprl 790 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑋)
120 simprr 792 . . . . . . . . . . . 12 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑐 ∈ (𝑁𝑞))
121 eleq1 2676 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
122121anbi2d 736 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → ((𝜑𝑝𝑋) ↔ (𝜑𝑞𝑋)))
123 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
124123eleq2d 2673 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑞)))
125122, 124anbi12d 743 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ↔ ((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞))))
126 elequ1 1984 . . . . . . . . . . . . . 14 (𝑝 = 𝑞 → (𝑝𝑐𝑞𝑐))
127125, 126imbi12d 333 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐) ↔ (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)))
128 elequ2 1991 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → (𝑝𝑎𝑝𝑐))
12974, 128imbi12d 333 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑝𝑎) ↔ (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)))
130129, 12chvarv 2251 . . . . . . . . . . . . 13 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → 𝑝𝑐)
131127, 130chvarv 2251 . . . . . . . . . . . 12 (((𝜑𝑞𝑋) ∧ 𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐)
132118, 119, 120, 131syl21anc 1317 . . . . . . . . . . 11 ((((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) ∧ (𝑞𝑋𝑐 ∈ (𝑁𝑞))) → 𝑞𝑐)
133132ex 449 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ((𝑞𝑋𝑐 ∈ (𝑁𝑞)) → 𝑞𝑐))
134117, 133syl5bi 231 . . . . . . . . 9 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑞 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → 𝑞𝑐))
135114, 115, 116, 134ssrd 3573 . . . . . . . 8 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)
136 eleq2 2677 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑝𝑑𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)}))
137 sseq1 3589 . . . . . . . . . 10 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → (𝑑𝑐 ↔ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐))
138136, 137anbi12d 743 . . . . . . . . 9 (𝑑 = {𝑞𝑋𝑐 ∈ (𝑁𝑞)} → ((𝑝𝑑𝑑𝑐) ↔ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)))
139138rspcev 3282 . . . . . . . 8 (({𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∈ 𝐽 ∧ (𝑝 ∈ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ∧ {𝑞𝑋𝑐 ∈ (𝑁𝑞)} ⊆ 𝑐)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
140107, 113, 135, 139syl12anc 1316 . . . . . . 7 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
14118, 140jca 553 . . . . . 6 (((𝜑𝑝𝑋) ∧ 𝑐 ∈ (𝑁𝑝)) → (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
142 nfv 1830 . . . . . . . 8 𝑑(𝜑𝑝𝑋)
143 nfv 1830 . . . . . . . . 9 𝑑 𝑐 𝐽
144 nfre1 2988 . . . . . . . . 9 𝑑𝑑𝐽 (𝑝𝑑𝑑𝑐)
145143, 144nfan 1816 . . . . . . . 8 𝑑(𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))
146142, 145nfan 1816 . . . . . . 7 𝑑((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)))
147 simplll 794 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → (𝜑𝑝𝑋))
148 simpr 476 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑𝑐)
149 simpr1l 1111 . . . . . . . . . 10 (((𝜑𝑝𝑋) ∧ ((𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐)) ∧ 𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐)) → 𝑐 𝐽)
1501493anassrs 1282 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 𝐽)
151147, 16syl 17 . . . . . . . . 9 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑋 = 𝐽)
152150, 151sseqtr4d 3605 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐𝑋)
153 simplr 788 . . . . . . . 8 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑑 ∈ (𝑁𝑝))
154 sseq1 3589 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (𝑎𝑐𝑑𝑐))
1551543anbi2d 1396 . . . . . . . . . . 11 (𝑎 = 𝑑 → (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋)))
156 eleq1 2676 . . . . . . . . . . 11 (𝑎 = 𝑑 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑑 ∈ (𝑁𝑝)))
157155, 156anbi12d 743 . . . . . . . . . 10 (𝑎 = 𝑑 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝))))
158157imbi1d 330 . . . . . . . . 9 (𝑎 = 𝑑 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
159 sseq2 3590 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑎𝑏𝑎𝑐))
160 sseq1 3589 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝑏𝑋𝑐𝑋))
161159, 1603anbi23d 1394 . . . . . . . . . . . 12 (𝑏 = 𝑐 → (((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋)))
162161anbi1d 737 . . . . . . . . . . 11 (𝑏 = 𝑐 → ((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝))))
163 eleq1 2676 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑐 ∈ (𝑁𝑝)))
164162, 163imbi12d 333 . . . . . . . . . 10 (𝑏 = 𝑐 → (((((𝜑𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))))
165164, 10chvarv 2251 . . . . . . . . 9 ((((𝜑𝑝𝑋) ∧ 𝑎𝑐𝑐𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
166158, 165chvarv 2251 . . . . . . . 8 ((((𝜑𝑝𝑋) ∧ 𝑑𝑐𝑐𝑋) ∧ 𝑑 ∈ (𝑁𝑝)) → 𝑐 ∈ (𝑁𝑝))
167147, 148, 152, 153, 166syl31anc 1321 . . . . . . 7 (((((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝑁𝑝)) ∧ 𝑑𝑐) → 𝑐 ∈ (𝑁𝑝))
1689neipeltop 20743 . . . . . . . . . . . . 13 (𝑑𝐽 ↔ (𝑑𝑋 ∧ ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝)))
169168simprbi 479 . . . . . . . . . . . 12 (𝑑𝐽 → ∀𝑝𝑑 𝑑 ∈ (𝑁𝑝))
170169r19.21bi 2916 . . . . . . . . . . 11 ((𝑑𝐽𝑝𝑑) → 𝑑 ∈ (𝑁𝑝))
171170anim1i 590 . . . . . . . . . 10 (((𝑑𝐽𝑝𝑑) ∧ 𝑑𝑐) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
172171anasss 677 . . . . . . . . 9 ((𝑑𝐽 ∧ (𝑝𝑑𝑑𝑐)) → (𝑑 ∈ (𝑁𝑝) ∧ 𝑑𝑐))
173172reximi2 2993 . . . . . . . 8 (∃𝑑𝐽 (𝑝𝑑𝑑𝑐) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
174173ad2antll 761 . . . . . . 7 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝑁𝑝)𝑑𝑐)
175146, 167, 174r19.29af 3058 . . . . . 6 (((𝜑𝑝𝑋) ∧ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))) → 𝑐 ∈ (𝑁𝑝))
176141, 175impbida 873 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
17735adantr 480 . . . . . 6 ((𝜑𝑝𝑋) → 𝐽 ∈ Top)
178108, 16eleqtrd 2690 . . . . . 6 ((𝜑𝑝𝑋) → 𝑝 𝐽)
179 eqid 2610 . . . . . . 7 𝐽 = 𝐽
180179isneip 20719 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑝 𝐽) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
181177, 178, 180syl2anc 691 . . . . 5 ((𝜑𝑝𝑋) → (𝑐 ∈ ((nei‘𝐽)‘{𝑝}) ↔ (𝑐 𝐽 ∧ ∃𝑑𝐽 (𝑝𝑑𝑑𝑐))))
182176, 181bitr4d 270 . . . 4 ((𝜑𝑝𝑋) → (𝑐 ∈ (𝑁𝑝) ↔ 𝑐 ∈ ((nei‘𝐽)‘{𝑝})))
183182eqrdv 2608 . . 3 ((𝜑𝑝𝑋) → (𝑁𝑝) = ((nei‘𝐽)‘{𝑝}))
184183mpteq2dva 4672 . 2 (𝜑 → (𝑝𝑋 ↦ (𝑁𝑝)) = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
1852, 184eqtrd 2644 1 (𝜑𝑁 = (𝑝𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  wss 3540  𝒫 cpw 4108  {csn 4125   cuni 4372  cmpt 4643  wf 5800  cfv 5804  ficfi 8199  Topctop 20517  neicnei 20711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845  df-fi 8200  df-top 20521  df-nei 20712
This theorem is referenced by:  neiptopreu  20747  utopsnneiplem  21861
  Copyright terms: Public domain W3C validator