Metamath Proof Explorer


Theorem cmpsub

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman'sBeginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis cmpsub.1 𝑋 = 𝐽
Assertion cmpsub ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐽t 𝑆 ) ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )

Proof

Step Hyp Ref Expression
1 cmpsub.1 𝑋 = 𝐽
2 eqid ( 𝐽t 𝑆 ) = ( 𝐽t 𝑆 )
3 2 iscmp ( ( 𝐽t 𝑆 ) ∈ Comp ↔ ( ( 𝐽t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
4 id ( 𝑆𝑋𝑆𝑋 )
5 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
6 ssexg ( ( 𝑆𝑋𝑋𝐽 ) → 𝑆 ∈ V )
7 4 5 6 syl2anr ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → 𝑆 ∈ V )
8 resttop ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐽t 𝑆 ) ∈ Top )
9 7 8 syldan ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝐽t 𝑆 ) ∈ Top )
10 ibar ( ( 𝐽t 𝑆 ) ∈ Top → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ↔ ( ( 𝐽t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) ) )
11 10 bicomd ( ( 𝐽t 𝑆 ) ∈ Top → ( ( ( 𝐽t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
12 9 11 syl ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( ( 𝐽t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
13 3 12 syl5bb ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐽t 𝑆 ) ∈ Comp ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
14 vex 𝑡 ∈ V
15 eqeq1 ( 𝑥 = 𝑡 → ( 𝑥 = ( 𝑦𝑆 ) ↔ 𝑡 = ( 𝑦𝑆 ) ) )
16 15 rexbidv ( 𝑥 = 𝑡 → ( ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) ↔ ∃ 𝑦𝑐 𝑡 = ( 𝑦𝑆 ) ) )
17 14 16 elab ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ↔ ∃ 𝑦𝑐 𝑡 = ( 𝑦𝑆 ) )
18 velpw ( 𝑐 ∈ 𝒫 𝐽𝑐𝐽 )
19 ssel2 ( ( 𝑐𝐽𝑦𝑐 ) → 𝑦𝐽 )
20 ineq1 ( 𝑑 = 𝑦 → ( 𝑑𝑆 ) = ( 𝑦𝑆 ) )
21 20 rspceeqv ( ( 𝑦𝐽𝑡 = ( 𝑦𝑆 ) ) → ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) )
22 21 ex ( 𝑦𝐽 → ( 𝑡 = ( 𝑦𝑆 ) → ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) )
23 19 22 syl ( ( 𝑐𝐽𝑦𝑐 ) → ( 𝑡 = ( 𝑦𝑆 ) → ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) )
24 23 ex ( 𝑐𝐽 → ( 𝑦𝑐 → ( 𝑡 = ( 𝑦𝑆 ) → ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) ) )
25 18 24 sylbi ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑦𝑐 → ( 𝑡 = ( 𝑦𝑆 ) → ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) ) )
26 25 adantl ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑦𝑐 → ( 𝑡 = ( 𝑦𝑆 ) → ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) ) )
27 26 rexlimdv ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∃ 𝑦𝑐 𝑡 = ( 𝑦𝑆 ) → ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) )
28 simpll ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → 𝐽 ∈ Top )
29 1 sseq2i ( 𝑆𝑋𝑆 𝐽 )
30 uniexg ( 𝐽 ∈ Top → 𝐽 ∈ V )
31 ssexg ( ( 𝑆 𝐽 𝐽 ∈ V ) → 𝑆 ∈ V )
32 30 31 sylan2 ( ( 𝑆 𝐽𝐽 ∈ Top ) → 𝑆 ∈ V )
33 32 ancoms ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → 𝑆 ∈ V )
34 29 33 sylan2b ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → 𝑆 ∈ V )
35 34 adantr ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → 𝑆 ∈ V )
36 elrest ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝑡 ∈ ( 𝐽t 𝑆 ) ↔ ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) )
37 28 35 36 syl2anc ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑡 ∈ ( 𝐽t 𝑆 ) ↔ ∃ 𝑑𝐽 𝑡 = ( 𝑑𝑆 ) ) )
38 27 37 sylibrd ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∃ 𝑦𝑐 𝑡 = ( 𝑦𝑆 ) → 𝑡 ∈ ( 𝐽t 𝑆 ) ) )
39 17 38 syl5bi ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → 𝑡 ∈ ( 𝐽t 𝑆 ) ) )
40 39 ssrdv ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ⊆ ( 𝐽t 𝑆 ) )
41 vex 𝑐 ∈ V
42 41 abrexex { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∈ V
43 42 elpw ( { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∈ 𝒫 ( 𝐽t 𝑆 ) ↔ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ⊆ ( 𝐽t 𝑆 ) )
44 40 43 sylibr ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∈ 𝒫 ( 𝐽t 𝑆 ) )
45 unieq ( 𝑠 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → 𝑠 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } )
46 45 eqeq2d ( 𝑠 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ( ( 𝐽t 𝑆 ) = 𝑠 ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ) )
47 pweq ( 𝑠 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → 𝒫 𝑠 = 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } )
48 47 ineq1d ( 𝑠 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) )
49 48 rexeqdv ( 𝑠 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ( ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ↔ ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) )
50 46 49 imbi12d ( 𝑠 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ( ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ↔ ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
51 50 rspcva ( ( { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∈ 𝒫 ( 𝐽t 𝑆 ) ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) → ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) )
52 44 51 sylan ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) → ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) )
53 52 ex ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) → ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
54 1 restuni ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → 𝑆 = ( 𝐽t 𝑆 ) )
55 54 ad2antrr ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → 𝑆 = ( 𝐽t 𝑆 ) )
56 vex 𝑦 ∈ V
57 56 inex1 ( 𝑦𝑆 ) ∈ V
58 57 dfiun2 𝑦𝑐 ( 𝑦𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) }
59 incom ( 𝑦𝑆 ) = ( 𝑆𝑦 )
60 59 a1i ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ 𝑦𝑐 ) → ( 𝑦𝑆 ) = ( 𝑆𝑦 ) )
61 60 iuneq2dv ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → 𝑦𝑐 ( 𝑦𝑆 ) = 𝑦𝑐 ( 𝑆𝑦 ) )
62 58 61 eqtr3id ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } = 𝑦𝑐 ( 𝑆𝑦 ) )
63 iunin2 𝑦𝑐 ( 𝑆𝑦 ) = ( 𝑆 𝑦𝑐 𝑦 )
64 uniiun 𝑐 = 𝑦𝑐 𝑦
65 64 eqcomi 𝑦𝑐 𝑦 = 𝑐
66 65 a1i ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → 𝑦𝑐 𝑦 = 𝑐 )
67 66 ineq2d ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( 𝑆 𝑦𝑐 𝑦 ) = ( 𝑆 𝑐 ) )
68 incom ( 𝑆 𝑐 ) = ( 𝑐𝑆 )
69 sseqin2 ( 𝑆 𝑐 ↔ ( 𝑐𝑆 ) = 𝑆 )
70 69 biimpi ( 𝑆 𝑐 → ( 𝑐𝑆 ) = 𝑆 )
71 68 70 syl5eq ( 𝑆 𝑐 → ( 𝑆 𝑐 ) = 𝑆 )
72 71 adantl ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( 𝑆 𝑐 ) = 𝑆 )
73 67 72 eqtrd ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( 𝑆 𝑦𝑐 𝑦 ) = 𝑆 )
74 63 73 syl5eq ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → 𝑦𝑐 ( 𝑆𝑦 ) = 𝑆 )
75 62 74 eqtr2d ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → 𝑆 = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } )
76 55 75 eqeq12d ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( 𝑆 = 𝑆 ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ) )
77 55 eqeq1d ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( 𝑆 = 𝑡 ( 𝐽t 𝑆 ) = 𝑡 ) )
78 77 rexbidv ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) 𝑆 = 𝑡 ↔ ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) )
79 76 78 imbi12d ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) 𝑆 = 𝑡 ) ↔ ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
80 eqid 𝑆 = 𝑆
81 80 a1bi ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) 𝑆 = 𝑡 ↔ ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) 𝑆 = 𝑡 ) )
82 elin ( 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ↔ ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∧ 𝑡 ∈ Fin ) )
83 velpw ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ↔ 𝑡 ⊆ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } )
84 dfss3 ( 𝑡 ⊆ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ↔ ∀ 𝑠𝑡 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } )
85 vex 𝑠 ∈ V
86 eqeq1 ( 𝑥 = 𝑠 → ( 𝑥 = ( 𝑦𝑆 ) ↔ 𝑠 = ( 𝑦𝑆 ) ) )
87 86 rexbidv ( 𝑥 = 𝑠 → ( ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) ↔ ∃ 𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ) )
88 85 87 elab ( 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ↔ ∃ 𝑦𝑐 𝑠 = ( 𝑦𝑆 ) )
89 88 ralbii ( ∀ 𝑠𝑡 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ↔ ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) )
90 83 84 89 3bitri ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ↔ ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) )
91 90 anbi1i ( ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∧ 𝑡 ∈ Fin ) ↔ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) )
92 82 91 bitri ( 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ↔ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) )
93 ineq1 ( 𝑦 = ( 𝑓𝑠 ) → ( 𝑦𝑆 ) = ( ( 𝑓𝑠 ) ∩ 𝑆 ) )
94 93 eqeq2d ( 𝑦 = ( 𝑓𝑠 ) → ( 𝑠 = ( 𝑦𝑆 ) ↔ 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) )
95 94 ac6sfi ( ( 𝑡 ∈ Fin ∧ ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ) → ∃ 𝑓 ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) )
96 95 ancoms ( ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) → ∃ 𝑓 ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) )
97 96 adantl ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ∃ 𝑓 ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) )
98 frn ( 𝑓 : 𝑡𝑐 → ran 𝑓𝑐 )
99 98 ad2antrl ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓𝑐 )
100 vex 𝑓 ∈ V
101 100 rnex ran 𝑓 ∈ V
102 101 elpw ( ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐 )
103 99 102 sylibr ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ 𝒫 𝑐 )
104 simprr ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) → 𝑡 ∈ Fin )
105 104 ad2antrr ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → 𝑡 ∈ Fin )
106 ffn ( 𝑓 : 𝑡𝑐𝑓 Fn 𝑡 )
107 dffn4 ( 𝑓 Fn 𝑡𝑓 : 𝑡onto→ ran 𝑓 )
108 106 107 sylib ( 𝑓 : 𝑡𝑐𝑓 : 𝑡onto→ ran 𝑓 )
109 fodomfi ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡onto→ ran 𝑓 ) → ran 𝑓𝑡 )
110 108 109 sylan2 ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡𝑐 ) → ran 𝑓𝑡 )
111 110 adantll ( ( ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ∧ 𝑓 : 𝑡𝑐 ) → ran 𝑓𝑡 )
112 111 adantll ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑓 : 𝑡𝑐 ) → ran 𝑓𝑡 )
113 112 ad2ant2r ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓𝑡 )
114 domfi ( ( 𝑡 ∈ Fin ∧ ran 𝑓𝑡 ) → ran 𝑓 ∈ Fin )
115 105 113 114 syl2anc ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ Fin )
116 103 115 elind ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) )
117 id ( 𝑠 = 𝑢𝑠 = 𝑢 )
118 fveq2 ( 𝑠 = 𝑢 → ( 𝑓𝑠 ) = ( 𝑓𝑢 ) )
119 118 ineq1d ( 𝑠 = 𝑢 → ( ( 𝑓𝑠 ) ∩ 𝑆 ) = ( ( 𝑓𝑢 ) ∩ 𝑆 ) )
120 117 119 eqeq12d ( 𝑠 = 𝑢 → ( 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ↔ 𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) )
121 120 rspccv ( ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) → ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) )
122 pm2.27 ( 𝑢𝑡 → ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) → 𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) )
123 inss1 ( ( 𝑓𝑢 ) ∩ 𝑆 ) ⊆ ( 𝑓𝑢 )
124 sseq1 ( 𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) → ( 𝑢 ⊆ ( 𝑓𝑢 ) ↔ ( ( 𝑓𝑢 ) ∩ 𝑆 ) ⊆ ( 𝑓𝑢 ) ) )
125 123 124 mpbiri ( 𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) → 𝑢 ⊆ ( 𝑓𝑢 ) )
126 ssel ( 𝑢 ⊆ ( 𝑓𝑢 ) → ( 𝑤𝑢𝑤 ∈ ( 𝑓𝑢 ) ) )
127 126 a1dd ( 𝑢 ⊆ ( 𝑓𝑢 ) → ( 𝑤𝑢 → ( 𝑓 : 𝑡𝑐𝑤 ∈ ( 𝑓𝑢 ) ) ) )
128 125 127 syl ( 𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) → ( 𝑤𝑢 → ( 𝑓 : 𝑡𝑐𝑤 ∈ ( 𝑓𝑢 ) ) ) )
129 128 a1i ( 𝑢𝑡 → ( 𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) → ( 𝑤𝑢 → ( 𝑓 : 𝑡𝑐𝑤 ∈ ( 𝑓𝑢 ) ) ) ) )
130 129 3imp ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ∧ 𝑤𝑢 ) → ( 𝑓 : 𝑡𝑐𝑤 ∈ ( 𝑓𝑢 ) ) )
131 fnfvelrn ( ( 𝑓 Fn 𝑡𝑢𝑡 ) → ( 𝑓𝑢 ) ∈ ran 𝑓 )
132 131 expcom ( 𝑢𝑡 → ( 𝑓 Fn 𝑡 → ( 𝑓𝑢 ) ∈ ran 𝑓 ) )
133 132 3ad2ant1 ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ∧ 𝑤𝑢 ) → ( 𝑓 Fn 𝑡 → ( 𝑓𝑢 ) ∈ ran 𝑓 ) )
134 106 133 syl5 ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ∧ 𝑤𝑢 ) → ( 𝑓 : 𝑡𝑐 → ( 𝑓𝑢 ) ∈ ran 𝑓 ) )
135 130 134 jcad ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ∧ 𝑤𝑢 ) → ( 𝑓 : 𝑡𝑐 → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) )
136 135 3exp ( 𝑢𝑡 → ( 𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) → ( 𝑤𝑢 → ( 𝑓 : 𝑡𝑐 → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) ) ) )
137 122 136 syld ( 𝑢𝑡 → ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) → ( 𝑤𝑢 → ( 𝑓 : 𝑡𝑐 → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) ) ) )
138 137 com3r ( 𝑤𝑢 → ( 𝑢𝑡 → ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡𝑐 → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) ) ) )
139 138 imp ( ( 𝑤𝑢𝑢𝑡 ) → ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡𝑐 → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) ) )
140 139 com3l ( ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡𝑐 → ( ( 𝑤𝑢𝑢𝑡 ) → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) ) )
141 140 impcom ( ( 𝑓 : 𝑡𝑐 ∧ ( 𝑢𝑡𝑢 = ( ( 𝑓𝑢 ) ∩ 𝑆 ) ) ) → ( ( 𝑤𝑢𝑢𝑡 ) → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) )
142 121 141 sylan2 ( ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ( ( 𝑤𝑢𝑢𝑡 ) → ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) )
143 fvex ( 𝑓𝑢 ) ∈ V
144 eleq2 ( 𝑣 = ( 𝑓𝑢 ) → ( 𝑤𝑣𝑤 ∈ ( 𝑓𝑢 ) ) )
145 eleq1 ( 𝑣 = ( 𝑓𝑢 ) → ( 𝑣 ∈ ran 𝑓 ↔ ( 𝑓𝑢 ) ∈ ran 𝑓 ) )
146 144 145 anbi12d ( 𝑣 = ( 𝑓𝑢 ) → ( ( 𝑤𝑣𝑣 ∈ ran 𝑓 ) ↔ ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) ) )
147 143 146 spcev ( ( 𝑤 ∈ ( 𝑓𝑢 ) ∧ ( 𝑓𝑢 ) ∈ ran 𝑓 ) → ∃ 𝑣 ( 𝑤𝑣𝑣 ∈ ran 𝑓 ) )
148 142 147 syl6 ( ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ( ( 𝑤𝑢𝑢𝑡 ) → ∃ 𝑣 ( 𝑤𝑣𝑣 ∈ ran 𝑓 ) ) )
149 148 exlimdv ( ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ( ∃ 𝑢 ( 𝑤𝑢𝑢𝑡 ) → ∃ 𝑣 ( 𝑤𝑣𝑣 ∈ ran 𝑓 ) ) )
150 eluni ( 𝑤 𝑡 ↔ ∃ 𝑢 ( 𝑤𝑢𝑢𝑡 ) )
151 eluni ( 𝑤 ran 𝑓 ↔ ∃ 𝑣 ( 𝑤𝑣𝑣 ∈ ran 𝑓 ) )
152 149 150 151 3imtr4g ( ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ( 𝑤 𝑡𝑤 ran 𝑓 ) )
153 152 ssrdv ( ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → 𝑡 ran 𝑓 )
154 153 adantl ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → 𝑡 ran 𝑓 )
155 sseq1 ( 𝑆 = 𝑡 → ( 𝑆 ran 𝑓 𝑡 ran 𝑓 ) )
156 155 ad2antlr ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → ( 𝑆 ran 𝑓 𝑡 ran 𝑓 ) )
157 154 156 mpbird ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → 𝑆 ran 𝑓 )
158 116 157 jca ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) ∧ ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) ) → ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ran 𝑓 ) )
159 158 ex ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) → ( ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ran 𝑓 ) ) )
160 159 eximdv ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = 𝑡 ) → ( ∃ 𝑓 ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ran 𝑓 ) ) )
161 160 ex ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( 𝑆 = 𝑡 → ( ∃ 𝑓 ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ran 𝑓 ) ) ) )
162 161 com23 ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ( 𝑆 = 𝑡 → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ran 𝑓 ) ) ) )
163 unieq ( 𝑑 = ran 𝑓 𝑑 = ran 𝑓 )
164 163 sseq2d ( 𝑑 = ran 𝑓 → ( 𝑆 𝑑𝑆 ran 𝑓 ) )
165 164 rspcev ( ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ran 𝑓 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 )
166 165 exlimiv ( ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ran 𝑓 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 )
167 162 166 syl8 ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡𝑐 ∧ ∀ 𝑠𝑡 𝑠 = ( ( 𝑓𝑠 ) ∩ 𝑆 ) ) → ( 𝑆 = 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )
168 97 167 mpd ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ ( ∀ 𝑠𝑡𝑦𝑐 𝑠 = ( 𝑦𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( 𝑆 = 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) )
169 92 168 sylan2b ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) ∧ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ) → ( 𝑆 = 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) )
170 169 rexlimdva ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) 𝑆 = 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) )
171 81 170 syl5bir ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) 𝑆 = 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) )
172 79 171 sylbird ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 𝑐 ) → ( ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) )
173 172 ex ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑆 𝑐 → ( ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )
174 173 com23 ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ( ( 𝐽t 𝑆 ) = { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦𝑐 𝑥 = ( 𝑦𝑆 ) } ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) → ( 𝑆 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )
175 53 174 syld ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) → ( 𝑆 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )
176 175 ralrimdva ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )
177 1 cmpsublem ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) → ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ) )
178 176 177 impbid ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽t 𝑆 ) ( ( 𝐽t 𝑆 ) = 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ( 𝐽t 𝑆 ) = 𝑡 ) ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )
179 13 178 bitrd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐽t 𝑆 ) ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 𝑑 ) ) )