This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neiptopnei

Description: Lemma for neiptopreu . (Contributed by Thierry Arnoux, 7-Jan-2018)

Ref Expression
Hypotheses neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
Assertion neiptopnei ( 𝜑 → 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
2 neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
3 neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
4 neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
5 neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
6 neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
7 neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
8 2 feqmptd ⊢ ( 𝜑 → 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑝 ) ) )
9 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑝 ) ∈ 𝒫 𝒫 𝑋 )
10 9 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑁 ‘ 𝑝 ) ∈ 𝒫 𝒫 𝑋 )
11 10 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑁 ‘ 𝑝 ) ⊆ 𝒫 𝑋 )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
13 11 12 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ∈ 𝒫 𝑋 )
14 13 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ⊆ 𝑋 )
15 1 2 3 4 5 6 7 neiptopuni ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 = ∪ 𝐽 )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑋 = ∪ 𝐽 )
18 14 17 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ⊆ ∪ 𝐽 )
19 ssrab2 ⊢ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋
20 19 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 )
21 fveq2 ⊢ ( 𝑞 = 𝑟 → ( 𝑁 ‘ 𝑞 ) = ( 𝑁 ‘ 𝑟 ) )
22 21 eleq2d ⊢ ( 𝑞 = 𝑟 → ( 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) )
23 22 elrab ⊢ ( 𝑟 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) )
24 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) → 𝜑 )
25 simpr1l ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) ) → 𝑟 ∈ 𝑋 )
26 25 3anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) → 𝑟 ∈ 𝑋 )
27 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) → 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
28 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) → 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) )
29 sseq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) )
30 29 3anbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ) )
31 eleq1w ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ↔ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) )
32 30 31 anbi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) ↔ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ) )
33 32 imbi1d ⊢ ( 𝑎 = 𝑏 → ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) ) ) )
34 simpl1l ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → 𝜑 )
35 1 2 3 4 5 6 7 neiptoptop ⊢ ( 𝜑 → 𝐽 ∈ Top )
36 35 uniexd ⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
37 15 36 eqeltrd ⊢ ( 𝜑 → 𝑋 ∈ V )
38 rabexg ⊢ ( 𝑋 ∈ V → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ V )
39 sseq2 ⊢ ( 𝑏 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( 𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) )
40 sseq1 ⊢ ( 𝑏 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( 𝑏 ⊆ 𝑋 ↔ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) )
41 39 40 3anbi23d ⊢ ( 𝑏 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ) )
42 41 anbi1d ⊢ ( 𝑏 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) ↔ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) ) )
43 eleq1 ⊢ ( 𝑏 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ↔ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) ) )
44 42 43 imbi12d ⊢ ( 𝑏 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) ) ) )
45 eleq1w ⊢ ( 𝑝 = 𝑟 → ( 𝑝 ∈ 𝑋 ↔ 𝑟 ∈ 𝑋 ) )
46 45 anbi2d ⊢ ( 𝑝 = 𝑟 → ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ) )
47 46 3anbi1d ⊢ ( 𝑝 = 𝑟 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ) )
48 fveq2 ⊢ ( 𝑝 = 𝑟 → ( 𝑁 ‘ 𝑝 ) = ( 𝑁 ‘ 𝑟 ) )
49 48 eleq2d ⊢ ( 𝑝 = 𝑟 → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) )
50 47 49 anbi12d ⊢ ( 𝑝 = 𝑟 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) ) )
51 48 eleq2d ⊢ ( 𝑝 = 𝑟 → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) )
52 50 51 imbi12d ⊢ ( 𝑝 = 𝑟 → ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ) )
53 52 3 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) )
54 44 53 vtoclg ⊢ ( { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ V → ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) ) )
55 37 38 54 3syl ⊢ ( 𝜑 → ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) ) )
56 34 55 mpcom ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑎 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
57 33 56 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
58 57 3an1rs ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
59 19 58 mpan2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
60 24 26 27 28 59 syl211anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
61 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) → 𝜑 )
62 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) → 𝑟 ∈ 𝑋 )
63 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) )
64 48 eleq2d ⊢ ( 𝑝 = 𝑟 → ( 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) )
65 46 64 anbi12d ⊢ ( 𝑝 = 𝑟 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) )
66 fveq2 ⊢ ( 𝑞 = 𝑠 → ( 𝑁 ‘ 𝑞 ) = ( 𝑁 ‘ 𝑠 ) )
67 66 eleq2d ⊢ ( 𝑞 = 𝑠 → ( 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) )
68 67 cbvralvw ⊢ ( ∀ 𝑞 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ↔ ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) )
69 68 a1i ⊢ ( 𝑝 = 𝑟 → ( ∀ 𝑞 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ↔ ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) )
70 48 69 rexeqbidv ⊢ ( 𝑝 = 𝑟 → ( ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ↔ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) )
71 65 70 imbi12d ⊢ ( 𝑝 = 𝑟 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) ↔ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) ) )
72 eleq1w ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) )
73 72 anbi2d ⊢ ( 𝑎 = 𝑐 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
74 eleq1w ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) )
75 74 rexralbidv ⊢ ( 𝑎 = 𝑐 → ( ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) ↔ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) )
76 73 75 imbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) ) ↔ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) ) )
77 76 6 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) )
78 71 77 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) )
79 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑟 ) ∈ 𝒫 𝒫 𝑋 )
80 79 elpwid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑟 ) ⊆ 𝒫 𝑋 )
81 80 sselda ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) → 𝑏 ∈ 𝒫 𝑋 )
82 81 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) → 𝑏 ⊆ 𝑋 )
83 82 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑠 ∈ 𝑏 ) → 𝑠 ∈ 𝑋 )
84 83 a1d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑠 ∈ 𝑏 ) → ( 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) → 𝑠 ∈ 𝑋 ) )
85 84 ancrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) ∧ 𝑠 ∈ 𝑏 ) → ( 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) → ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) ) )
86 85 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ) → ( ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) → ∀ 𝑠 ∈ 𝑏 ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) ) )
87 86 reximdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) → ( ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) ) )
88 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) → ( ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) ) )
89 78 88 mpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) )
90 67 elrab ⊢ ( 𝑠 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) )
91 90 ralbii ⊢ ( ∀ 𝑠 ∈ 𝑏 𝑠 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ ∀ 𝑠 ∈ 𝑏 ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) )
92 91 rexbii ⊢ ( ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑠 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 ( 𝑠 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑠 ) ) )
93 89 92 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑠 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
94 dfss3 ⊢ ( 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ ∀ 𝑠 ∈ 𝑏 𝑠 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
95 94 biimpri ⊢ ( ∀ 𝑠 ∈ 𝑏 𝑠 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
96 95 reximi ⊢ ( ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) ∀ 𝑠 ∈ 𝑏 𝑠 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
97 93 96 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
98 61 62 63 97 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑟 ) 𝑏 ⊆ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
99 60 98 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
100 23 99 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑟 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
101 100 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∀ 𝑟 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
102 48 eleq2d ⊢ ( 𝑝 = 𝑟 → ( { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑝 ) ↔ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) ) )
103 102 cbvralvw ⊢ ( ∀ 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∀ 𝑟 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑟 ) )
104 101 103 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∀ 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑝 ) )
105 1 neipeltop ⊢ ( { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ 𝐽 ↔ ( { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑋 ∧ ∀ 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ ( 𝑁 ‘ 𝑝 ) ) )
106 20 104 105 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ 𝐽 )
107 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ 𝑋 )
108 107 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑝 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) )
109 fveq2 ⊢ ( 𝑞 = 𝑝 → ( 𝑁 ‘ 𝑞 ) = ( 𝑁 ‘ 𝑝 ) )
110 109 eleq2d ⊢ ( 𝑞 = 𝑝 → ( 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) )
111 110 elrab ⊢ ( 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ ( 𝑝 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) )
112 108 111 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } )
113 nfv ⊢ Ⅎ 𝑞 ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
114 nfrab1 ⊢ Ⅎ 𝑞 { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) }
115 nfcv ⊢ Ⅎ 𝑞 𝑐
116 rabid ⊢ ( 𝑞 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ↔ ( 𝑞 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) )
117 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) ) → 𝜑 )
118 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) ) → 𝑞 ∈ 𝑋 )
119 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) )
120 eleq1w ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋 ) )
121 120 anbi2d ⊢ ( 𝑝 = 𝑞 → ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑞 ∈ 𝑋 ) ) )
122 fveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝑁 ‘ 𝑝 ) = ( 𝑁 ‘ 𝑞 ) )
123 122 eleq2d ⊢ ( 𝑝 = 𝑞 → ( 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) )
124 121 123 anbi12d ⊢ ( 𝑝 = 𝑞 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( 𝜑 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) ) )
125 elequ1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∈ 𝑐 ↔ 𝑞 ∈ 𝑐 ) )
126 124 125 imbi12d ⊢ ( 𝑝 = 𝑞 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑐 ) ↔ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) → 𝑞 ∈ 𝑐 ) ) )
127 elequ2 ⊢ ( 𝑎 = 𝑐 → ( 𝑝 ∈ 𝑎 ↔ 𝑝 ∈ 𝑐 ) )
128 73 127 imbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 ) ↔ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑐 ) ) )
129 128 5 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑐 )
130 126 129 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) → 𝑞 ∈ 𝑐 )
131 117 118 119 130 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) ) → 𝑞 ∈ 𝑐 )
132 131 ex ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( ( 𝑞 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) ) → 𝑞 ∈ 𝑐 ) )
133 116 132 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑞 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → 𝑞 ∈ 𝑐 ) )
134 113 114 115 133 ssrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑐 )
135 eleq2 ⊢ ( 𝑑 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( 𝑝 ∈ 𝑑 ↔ 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ) )
136 sseq1 ⊢ ( 𝑑 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( 𝑑 ⊆ 𝑐 ↔ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑐 ) )
137 135 136 anbi12d ⊢ ( 𝑑 = { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } → ( ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ↔ ( 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑐 ) ) )
138 137 rspcev ⊢ ( ( { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∈ 𝐽 ∧ ( 𝑝 ∈ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ∧ { 𝑞 ∈ 𝑋 ∣ 𝑐 ∈ ( 𝑁 ‘ 𝑞 ) } ⊆ 𝑐 ) ) → ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) )
139 106 112 134 138 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) )
140 18 139 jca ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) )
141 nfv ⊢ Ⅎ 𝑑 ( 𝜑 ∧ 𝑝 ∈ 𝑋 )
142 nfv ⊢ Ⅎ 𝑑 𝑐 ⊆ ∪ 𝐽
143 nfre1 ⊢ Ⅎ 𝑑 ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 )
144 142 143 nfan ⊢ Ⅎ 𝑑 ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) )
145 141 144 nfan ⊢ Ⅎ 𝑑 ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) )
146 simplll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑑 ⊆ 𝑐 ) → ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) )
147 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑑 ⊆ 𝑐 ) → 𝑑 ⊆ 𝑐 )
148 simpr1l ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑑 ⊆ 𝑐 ) ) → 𝑐 ⊆ ∪ 𝐽 )
149 148 3anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑑 ⊆ 𝑐 ) → 𝑐 ⊆ ∪ 𝐽 )
150 146 16 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑑 ⊆ 𝑐 ) → 𝑋 = ∪ 𝐽 )
151 149 150 sseqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑑 ⊆ 𝑐 ) → 𝑐 ⊆ 𝑋 )
152 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑑 ⊆ 𝑐 ) → 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) )
153 sseq1 ⊢ ( 𝑎 = 𝑑 → ( 𝑎 ⊆ 𝑐 ↔ 𝑑 ⊆ 𝑐 ) )
154 153 3anbi2d ⊢ ( 𝑎 = 𝑑 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ) )
155 eleq1w ⊢ ( 𝑎 = 𝑑 → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) )
156 154 155 anbi12d ⊢ ( 𝑎 = 𝑑 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
157 156 imbi1d ⊢ ( 𝑎 = 𝑑 → ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
158 sseq2 ⊢ ( 𝑏 = 𝑐 → ( 𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ 𝑐 ) )
159 sseq1 ⊢ ( 𝑏 = 𝑐 → ( 𝑏 ⊆ 𝑋 ↔ 𝑐 ⊆ 𝑋 ) )
160 158 159 3anbi23d ⊢ ( 𝑏 = 𝑐 → ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ) )
161 160 anbi1d ⊢ ( 𝑏 = 𝑐 → ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
162 eleq1w ⊢ ( 𝑏 = 𝑐 → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) )
163 161 162 imbi12d ⊢ ( 𝑏 = 𝑐 → ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
164 163 3 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
165 157 164 chvarvv ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑑 ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑋 ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
166 146 147 151 152 165 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) ∧ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑑 ⊆ 𝑐 ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
167 1 neipeltop ⊢ ( 𝑑 ∈ 𝐽 ↔ ( 𝑑 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑑 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ) )
168 167 simprbi ⊢ ( 𝑑 ∈ 𝐽 → ∀ 𝑝 ∈ 𝑑 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) )
169 168 r19.21bi ⊢ ( ( 𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑 ) → 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) )
170 169 anim1i ⊢ ( ( ( 𝑑 ∈ 𝐽 ∧ 𝑝 ∈ 𝑑 ) ∧ 𝑑 ⊆ 𝑐 ) → ( 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑑 ⊆ 𝑐 ) )
171 170 anasss ⊢ ( ( 𝑑 ∈ 𝐽 ∧ ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) → ( 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝑑 ⊆ 𝑐 ) )
172 171 reximi2 ⊢ ( ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) → ∃ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) 𝑑 ⊆ 𝑐 )
173 172 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) → ∃ 𝑑 ∈ ( 𝑁 ‘ 𝑝 ) 𝑑 ⊆ 𝑐 )
174 145 166 173 r19.29af ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) → 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) )
175 140 174 impbida ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) )
176 107 16 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ ∪ 𝐽 )
177 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
178 177 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ ∪ 𝐽 ) → ( 𝑐 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ↔ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) )
179 35 176 178 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑐 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ↔ ( 𝑐 ⊆ ∪ 𝐽 ∧ ∃ 𝑑 ∈ 𝐽 ( 𝑝 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑐 ) ) ) )
180 175 179 bitr4d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑐 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
181 180 eqrdv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) )
182 181 mpteq2dva ⊢ ( 𝜑 → ( 𝑝 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
183 8 182 eqtrd ⊢ ( 𝜑 → 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )