Metamath Proof Explorer

Theorem neibastop1

Description: A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard'sGeneral Topology. (Contributed by Jeff Hankins, 8-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses neibastop1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
Assertion neibastop1 ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 neibastop1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
3 neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
4 neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
5 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → 𝑦 ⊆ 𝐽 )
6 ssrab2 ⊢ { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ } ⊆ 𝒫 𝑋
7 4 6 eqsstri ⊢ 𝐽 ⊆ 𝒫 𝑋
8 5 7 sstrdi ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → 𝑦 ⊆ 𝒫 𝑋 )
9 sspwuni ⊢ ( 𝑦 ⊆ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 )
10 8 9 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → ∪ 𝑦 ⊆ 𝑋 )
11 vuniex ⊢ ∪ 𝑦 ∈ V
12 11 elpw ⊢ ( ∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 )
13 10 12 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → ∪ 𝑦 ∈ 𝒫 𝑋 )
14 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝑦 ↔ ∃ 𝑧 ∈ 𝑦 𝑥 ∈ 𝑧 )
15 elssuni ⊢ ( 𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦 )
16 15 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑧 ⊆ ∪ 𝑦 )
17 16 sspwd ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → 𝒫 𝑧 ⊆ 𝒫 ∪ 𝑦 )
18 sslin ⊢ ( 𝒫 𝑧 ⊆ 𝒫 ∪ 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) )
19 17 18 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) )
20 5 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝐽 )
21 20 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑧 ∈ 𝐽 )
22 pweq ⊢ ( 𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧 )
23 22 ineq2d ⊢ ( 𝑜 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
24 23 neeq1d ⊢ ( 𝑜 = 𝑧 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
25 24 raleqbi1dv ⊢ ( 𝑜 = 𝑧 → ( ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
26 25 4 elrab2 ⊢ ( 𝑧 ∈ 𝐽 ↔ ( 𝑧 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
27 26 simprbi ⊢ ( 𝑧 ∈ 𝐽 → ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ )
28 21 27 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ )
29 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑥 ∈ 𝑧 )
30 rsp ⊢ ( ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ → ( 𝑥 ∈ 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
31 28 29 30 sylc ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ )
32 ssn0 ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ )
33 19 31 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ )
34 33 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → ( ∃ 𝑧 ∈ 𝑦 𝑥 ∈ 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ ) )
35 14 34 biimtrid ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → ( 𝑥 ∈ ∪ 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ ) )
36 35 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → ∀ 𝑥 ∈ ∪ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ )
37 pweq ⊢ ( 𝑜 = ∪ 𝑦 → 𝒫 𝑜 = 𝒫 ∪ 𝑦 )
38 37 ineq2d ⊢ ( 𝑜 = ∪ 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) )
39 38 neeq1d ⊢ ( 𝑜 = ∪ 𝑦 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ ) )
40 39 raleqbi1dv ⊢ ( 𝑜 = ∪ 𝑦 → ( ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ∀ 𝑥 ∈ ∪ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ ) )
41 40 4 elrab2 ⊢ ( ∪ 𝑦 ∈ 𝐽 ↔ ( ∪ 𝑦 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ ∪ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ∪ 𝑦 ) ≠ ∅ ) )
42 13 36 41 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐽 ) → ∪ 𝑦 ∈ 𝐽 )
43 42 ex ⊢ ( 𝜑 → ( 𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽 ) )
44 43 alrimiv ⊢ ( 𝜑 → ∀ 𝑦 ( 𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽 ) )
45 pweq ⊢ ( 𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦 )
46 45 ineq2d ⊢ ( 𝑜 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) )
47 46 neeq1d ⊢ ( 𝑜 = 𝑦 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
48 47 raleqbi1dv ⊢ ( 𝑜 = 𝑦 → ( ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
49 48 4 elrab2 ⊢ ( 𝑦 ∈ 𝐽 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
50 49 26 anbi12i ⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽 ) ↔ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) ∧ ( 𝑧 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) )
51 an4 ⊢ ( ( ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) ∧ ( 𝑧 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) ↔ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) )
52 50 51 bitri ⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽 ) ↔ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) )
53 inss1 ⊢ ( 𝑦 ∩ 𝑧 ) ⊆ 𝑦
54 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
55 53 54 sstrid ⊢ ( 𝑦 ∈ 𝒫 𝑋 → ( 𝑦 ∩ 𝑧 ) ⊆ 𝑋 )
56 55 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ 𝑋 )
57 56 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ 𝑋 )
58 vex ⊢ 𝑦 ∈ V
59 58 inex1 ⊢ ( 𝑦 ∩ 𝑧 ) ∈ V
60 59 elpw ⊢ ( ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝑋 ↔ ( 𝑦 ∩ 𝑧 ) ⊆ 𝑋 )
61 57 60 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝑋 )
62 ssralv ⊢ ( ( 𝑦 ∩ 𝑧 ) ⊆ 𝑦 → ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ) )
63 53 62 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ )
64 inss2 ⊢ ( 𝑦 ∩ 𝑧 ) ⊆ 𝑧
65 ssralv ⊢ ( ( 𝑦 ∩ 𝑧 ) ⊆ 𝑧 → ( ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
66 64 65 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ )
67 63 66 anim12i ⊢ ( ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) → ( ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
68 r19.26 ⊢ ( ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ↔ ( ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
69 67 68 sylibr ⊢ ( ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) )
70 n0 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) )
71 n0 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
72 70 71 anbi12i ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ↔ ( ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ ∃ 𝑤 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) )
73 exdistrv ⊢ ( ∃ 𝑣 ∃ 𝑤 ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ↔ ( ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ ∃ 𝑤 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) )
74 inss2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ⊆ 𝒫 𝑦
75 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) )
76 74 75 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑣 ∈ 𝒫 𝑦 )
77 76 elpwid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑣 ⊆ 𝑦 )
78 inss2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑧
79 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
80 78 79 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ 𝒫 𝑧 )
81 80 elpwid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ⊆ 𝑧 )
82 ss2in ⊢ ( ( 𝑣 ⊆ 𝑦 ∧ 𝑤 ⊆ 𝑧 ) → ( 𝑣 ∩ 𝑤 ) ⊆ ( 𝑦 ∩ 𝑧 ) )
83 77 81 82 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝑣 ∩ 𝑤 ) ⊆ ( 𝑦 ∩ 𝑧 ) )
84 83 sspwd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝒫 ( 𝑣 ∩ 𝑤 ) ⊆ 𝒫 ( 𝑦 ∩ 𝑧 ) )
85 sslin ⊢ ( 𝒫 ( 𝑣 ∩ 𝑤 ) ⊆ 𝒫 ( 𝑦 ∩ 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ⊆ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) )
86 84 85 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ⊆ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) )
87 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝜑 )
88 56 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ 𝑋 )
89 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) )
90 88 89 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑥 ∈ 𝑋 )
91 inss1 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 )
92 91 75 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) )
93 inss1 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ ( 𝐹 ‘ 𝑥 )
94 93 79 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) )
95 87 90 92 94 3 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
96 ssn0 ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ⊆ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ )
97 86 95 96 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) ∧ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ )
98 97 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) → ( ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
99 98 exlimdvv ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) → ( ∃ 𝑣 ∃ 𝑤 ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
100 73 99 biimtrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) → ( ( ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ∧ ∃ 𝑤 𝑤 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
101 72 100 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
102 101 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) → ( ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
103 69 102 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ) → ( ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
104 103 impr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) ) → ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ )
105 pweq ⊢ ( 𝑜 = ( 𝑦 ∩ 𝑧 ) → 𝒫 𝑜 = 𝒫 ( 𝑦 ∩ 𝑧 ) )
106 105 ineq2d ⊢ ( 𝑜 = ( 𝑦 ∩ 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) )
107 106 neeq1d ⊢ ( 𝑜 = ( 𝑦 ∩ 𝑧 ) → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
108 107 raleqbi1dv ⊢ ( 𝑜 = ( 𝑦 ∩ 𝑧 ) → ( ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
109 108 4 elrab2 ⊢ ( ( 𝑦 ∩ 𝑧 ) ∈ 𝐽 ↔ ( ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ ( 𝑦 ∩ 𝑧 ) ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) )
110 61 104 109 sylanbrc ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑦 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ≠ ∅ ) ) ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝐽 )
111 52 110 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝐽 )
112 111 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ 𝐽 ( 𝑦 ∩ 𝑧 ) ∈ 𝐽 )
113 sspwuni ⊢ ( 𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋 )
114 7 113 mpbi ⊢ ∪ 𝐽 ⊆ 𝑋
115 114 a1i ⊢ ( 𝜑 → ∪ 𝐽 ⊆ 𝑋 )
116 1 115 ssexd ⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
117 uniexb ⊢ ( 𝐽 ∈ V ↔ ∪ 𝐽 ∈ V )
118 116 117 sylibr ⊢ ( 𝜑 → 𝐽 ∈ V )
119 istopg ⊢ ( 𝐽 ∈ V → ( 𝐽 ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽 ) ∧ ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ 𝐽 ( 𝑦 ∩ 𝑧 ) ∈ 𝐽 ) ) )
120 118 119 syl ⊢ ( 𝜑 → ( 𝐽 ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ 𝐽 → ∪ 𝑦 ∈ 𝐽 ) ∧ ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ 𝐽 ( 𝑦 ∩ 𝑧 ) ∈ 𝐽 ) ) )
121 44 112 120 mpbir2and ⊢ ( 𝜑 → 𝐽 ∈ Top )
122 pwidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ 𝒫 𝑋 )
123 1 122 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝑋 )
124 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
125 eldifi ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝒫 𝒫 𝑋 )
126 elpwi ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝒫 𝒫 𝑋 → ( 𝐹 ‘ 𝑥 ) ⊆ 𝒫 𝑋 )
127 124 125 126 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ⊆ 𝒫 𝑋 )
128 dfss2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ⊆ 𝒫 𝑋 ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) = ( 𝐹 ‘ 𝑥 ) )
129 127 128 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) = ( 𝐹 ‘ 𝑥 ) )
130 eldifsni ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) → ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
131 124 130 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
132 129 131 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) ≠ ∅ )
133 132 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) ≠ ∅ )
134 pweq ⊢ ( 𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋 )
135 134 ineq2d ⊢ ( 𝑜 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) )
136 135 neeq1d ⊢ ( 𝑜 = 𝑋 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) ≠ ∅ ) )
137 136 raleqbi1dv ⊢ ( 𝑜 = 𝑋 → ( ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) ≠ ∅ ) )
138 137 4 elrab2 ⊢ ( 𝑋 ∈ 𝐽 ↔ ( 𝑋 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑋 ) ≠ ∅ ) )
139 123 133 138 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
140 elssuni ⊢ ( 𝑋 ∈ 𝐽 → 𝑋 ⊆ ∪ 𝐽 )
141 139 140 syl ⊢ ( 𝜑 → 𝑋 ⊆ ∪ 𝐽 )
142 141 115 eqssd ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
143 istopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽 ) )
144 121 142 143 sylanbrc ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )