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

Theorem cmpsub 23408
Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
Hypothesis
Ref Expression
cmpsub.1 𝑋 = 𝐽
Assertion
Ref Expression
cmpsub ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
Distinct variable groups:   𝑐,𝑑,𝐽   𝑆,𝑐,𝑑   𝑋,𝑐,𝑑

Proof of Theorem cmpsub
Dummy variables 𝑥 𝑦 𝑓 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . . . 4 (𝐽t 𝑆) = (𝐽t 𝑆)
21iscmp 23396 . . 3 ((𝐽t 𝑆) ∈ Comp ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
3 id 22 . . . . . 6 (𝑆𝑋𝑆𝑋)
4 cmpsub.1 . . . . . . 7 𝑋 = 𝐽
54topopn 22912 . . . . . 6 (𝐽 ∈ Top → 𝑋𝐽)
6 ssexg 5323 . . . . . 6 ((𝑆𝑋𝑋𝐽) → 𝑆 ∈ V)
73, 5, 6syl2anr 597 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
8 resttop 23168 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽t 𝑆) ∈ Top)
97, 8syldan 591 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝐽t 𝑆) ∈ Top)
10 ibar 528 . . . . 5 ((𝐽t 𝑆) ∈ Top → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡))))
1110bicomd 223 . . . 4 ((𝐽t 𝑆) ∈ Top → (((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
129, 11syl 17 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
132, 12bitrid 283 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
14 vex 3484 . . . . . . . . . . 11 𝑡 ∈ V
15 eqeq1 2741 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 = (𝑦𝑆) ↔ 𝑡 = (𝑦𝑆)))
1615rexbidv 3179 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆)))
1714, 16elab 3679 . . . . . . . . . 10 (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆))
18 velpw 4605 . . . . . . . . . . . . . 14 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
19 ssel2 3978 . . . . . . . . . . . . . . . 16 ((𝑐𝐽𝑦𝑐) → 𝑦𝐽)
20 ineq1 4213 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑦 → (𝑑𝑆) = (𝑦𝑆))
2120rspceeqv 3645 . . . . . . . . . . . . . . . . 17 ((𝑦𝐽𝑡 = (𝑦𝑆)) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))
2221ex 412 . . . . . . . . . . . . . . . 16 (𝑦𝐽 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((𝑐𝐽𝑦𝑐) → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2423ex 412 . . . . . . . . . . . . . 14 (𝑐𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2518, 24sylbi 217 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2625adantl 481 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2726rexlimdv 3153 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
28 simpll 767 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
294sseq2i 4013 . . . . . . . . . . . . . 14 (𝑆𝑋𝑆 𝐽)
30 uniexg 7760 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → 𝐽 ∈ V)
31 ssexg 5323 . . . . . . . . . . . . . . . 16 ((𝑆 𝐽 𝐽 ∈ V) → 𝑆 ∈ V)
3230, 31sylan2 593 . . . . . . . . . . . . . . 15 ((𝑆 𝐽𝐽 ∈ Top) → 𝑆 ∈ V)
3332ancoms 458 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → 𝑆 ∈ V)
3429, 33sylan2b 594 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
3534adantr 480 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V)
36 elrest 17472 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3728, 35, 36syl2anc 584 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3827, 37sylibrd 259 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → 𝑡 ∈ (𝐽t 𝑆)))
3917, 38biimtrid 242 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑡 ∈ (𝐽t 𝑆)))
4039ssrdv 3989 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
41 vex 3484 . . . . . . . . . 10 𝑐 ∈ V
4241abrexex 7987 . . . . . . . . 9 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ V
4342elpw 4604 . . . . . . . 8 ({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ↔ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
4440, 43sylibr 234 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆))
45 unieq 4918 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4645eqeq2d 2748 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ( (𝐽t 𝑆) = 𝑠 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
47 pweq 4614 . . . . . . . . . . 11 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4847ineq1d 4219 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin))
4948rexeqdv 3327 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5046, 49imbi12d 344 . . . . . . . 8 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
5150rspcva 3620 . . . . . . 7 (({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5244, 51sylan 580 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5352ex 412 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
544restuni 23170 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 = (𝐽t 𝑆))
5554ad2antrr 726 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = (𝐽t 𝑆))
56 vex 3484 . . . . . . . . . . . . . 14 𝑦 ∈ V
5756inex1 5317 . . . . . . . . . . . . 13 (𝑦𝑆) ∈ V
5857dfiun2 5033 . . . . . . . . . . . 12 𝑦𝑐 (𝑦𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}
59 incom 4209 . . . . . . . . . . . . . 14 (𝑦𝑆) = (𝑆𝑦)
6059a1i 11 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑦𝑐) → (𝑦𝑆) = (𝑆𝑦))
6160iuneq2dv 5016 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑦𝑆) = 𝑦𝑐 (𝑆𝑦))
6258, 61eqtr3id 2791 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} = 𝑦𝑐 (𝑆𝑦))
63 iunin2 5071 . . . . . . . . . . . 12 𝑦𝑐 (𝑆𝑦) = (𝑆 𝑦𝑐 𝑦)
64 uniiun 5058 . . . . . . . . . . . . . . . 16 𝑐 = 𝑦𝑐 𝑦
6564eqcomi 2746 . . . . . . . . . . . . . . 15 𝑦𝑐 𝑦 = 𝑐
6665a1i 11 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 𝑦 = 𝑐)
6766ineq2d 4220 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = (𝑆 𝑐))
68 incom 4209 . . . . . . . . . . . . . . 15 (𝑆 𝑐) = ( 𝑐𝑆)
69 sseqin2 4223 . . . . . . . . . . . . . . . 16 (𝑆 𝑐 ↔ ( 𝑐𝑆) = 𝑆)
7069biimpi 216 . . . . . . . . . . . . . . 15 (𝑆 𝑐 → ( 𝑐𝑆) = 𝑆)
7168, 70eqtrid 2789 . . . . . . . . . . . . . 14 (𝑆 𝑐 → (𝑆 𝑐) = 𝑆)
7271adantl 481 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑐) = 𝑆)
7367, 72eqtrd 2777 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = 𝑆)
7463, 73eqtrid 2789 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑆𝑦) = 𝑆)
7562, 74eqtr2d 2778 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
7655, 75eqeq12d 2753 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑆 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
7755eqeq1d 2739 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑡 (𝐽t 𝑆) = 𝑡))
7877rexbidv 3179 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
7976, 78imbi12d 344 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
80 eqid 2737 . . . . . . . . . 10 𝑆 = 𝑆
8180a1bi 362 . . . . . . . . 9 (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡))
82 elin 3967 . . . . . . . . . . . 12 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin))
83 velpw 4605 . . . . . . . . . . . . . 14 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
84 dfss3 3972 . . . . . . . . . . . . . 14 (𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
85 vex 3484 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
86 eqeq1 2741 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (𝑥 = (𝑦𝑆) ↔ 𝑠 = (𝑦𝑆)))
8786rexbidv 3179 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑠 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆)))
8885, 87elab 3679 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆))
8988ralbii 3093 . . . . . . . . . . . . . 14 (∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9083, 84, 893bitri 297 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9190anbi1i 624 . . . . . . . . . . . 12 ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
9282, 91bitri 275 . . . . . . . . . . 11 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
93 ineq1 4213 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑓𝑠) → (𝑦𝑆) = ((𝑓𝑠) ∩ 𝑆))
9493eqeq2d 2748 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝑠) → (𝑠 = (𝑦𝑆) ↔ 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9594ac6sfi 9320 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9695ancoms 458 . . . . . . . . . . . . 13 ((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9796adantl 481 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
98 frn 6743 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑡𝑐 → ran 𝑓𝑐)
9998ad2antrl 728 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑐)
100 vex 3484 . . . . . . . . . . . . . . . . . . . . . 22 𝑓 ∈ V
101100rnex 7932 . . . . . . . . . . . . . . . . . . . . 21 ran 𝑓 ∈ V
102101elpw 4604 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐)
10399, 102sylibr 234 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐)
104 simprr 773 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin)
105104ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin)
106 ffn 6736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑡𝑐𝑓 Fn 𝑡)
107 dffn4 6826 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑡𝑓:𝑡onto→ran 𝑓)
108106, 107sylib 218 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝑡𝑐𝑓:𝑡onto→ran 𝑓)
109 fodomfi 9350 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ Fin ∧ 𝑓:𝑡onto→ran 𝑓) → ran 𝑓𝑡)
110108, 109sylan2 593 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ Fin ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
111110adantll 714 . . . . . . . . . . . . . . . . . . . . . 22 (((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
112111adantll 714 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
113112ad2ant2r 747 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑡)
114 domfi 9229 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ran 𝑓𝑡) → ran 𝑓 ∈ Fin)
115105, 113, 114syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
116103, 115elind 4200 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
117 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢𝑠 = 𝑢)
118 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = 𝑢 → (𝑓𝑠) = (𝑓𝑢))
119118ineq1d 4219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢 → ((𝑓𝑠) ∩ 𝑆) = ((𝑓𝑢) ∩ 𝑆))
120117, 119eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑢 → (𝑠 = ((𝑓𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
121120rspccv 3619 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆) → (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)))
122 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
123 inss1 4237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)
124 sseq1 4009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓𝑢) ↔ ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)))
125123, 124mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓𝑢))
126 ssel 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢𝑤 ∈ (𝑓𝑢)))
127126a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
128125, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
129128a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))))
1301293imp 1111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))
131 fnfvelrn 7100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓 Fn 𝑡𝑢𝑡) → (𝑓𝑢) ∈ ran 𝑓)
132131expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢𝑡 → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
1331323ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
134106, 133syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑓𝑢) ∈ ran 𝑓))
135130, 134jcad 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
1361353exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
137122, 136syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
138137com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑢 → (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
139138imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤𝑢𝑢𝑡) → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
140139com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
141140impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑡𝑐 ∧ (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆))) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
142121, 141sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
143 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓𝑢) ∈ V
144 eleq2 2830 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑤𝑣𝑤 ∈ (𝑓𝑢)))
145 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓𝑢) ∈ ran 𝑓))
146144, 145anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = (𝑓𝑢) → ((𝑤𝑣𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
147143, 146spcev 3606 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
148142, 147syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
149148exlimdv 1933 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (∃𝑢(𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
150 eluni 4910 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑡 ↔ ∃𝑢(𝑤𝑢𝑢𝑡))
151 eluni 4910 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ran 𝑓 ↔ ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
152149, 150, 1513imtr4g 296 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑤 𝑡𝑤 ran 𝑓))
153152ssrdv 3989 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → 𝑡 ran 𝑓)
154153adantl 481 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ran 𝑓)
155 sseq1 4009 . . . . . . . . . . . . . . . . . . . 20 (𝑆 = 𝑡 → (𝑆 ran 𝑓 𝑡 ran 𝑓))
156155ad2antlr 727 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (𝑆 ran 𝑓 𝑡 ran 𝑓))
157154, 156mpbird 257 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑆 ran 𝑓)
158116, 157jca 511 . . . . . . . . . . . . . . . . 17 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))
159158ex 412 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
160159eximdv 1917 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
161160ex 412 . . . . . . . . . . . . . 14 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
162161com23 86 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
163 unieq 4918 . . . . . . . . . . . . . . . 16 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
164163sseq2d 4016 . . . . . . . . . . . . . . 15 (𝑑 = ran 𝑓 → (𝑆 𝑑𝑆 ran 𝑓))
165164rspcev 3622 . . . . . . . . . . . . . 14 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
166165exlimiv 1930 . . . . . . . . . . . . 13 (∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
167162, 166syl8 76 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
16897, 167mpd 15 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
16992, 168sylan2b 594 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
170169rexlimdva 3155 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17181, 170biimtrrid 243 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17279, 171sylbird 260 . . . . . . 7 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
173172ex 412 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑆 𝑐 → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
174173com23 86 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → (𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
17553, 174syld 47 . . . 4 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → (𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
176175ralrimdva 3154 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
1774cmpsublem 23407 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
178176, 177impbid 212 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
17913, 178bitrd 279 1 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wral 3061  wrex 3070  Vcvv 3480  cin 3950  wss 3951  𝒫 cpw 4600   cuni 4907   ciun 4991   class class class wbr 5143  ran crn 5686   Fn wfn 6556  wf 6557  ontowfo 6559  cfv 6561  (class class class)co 7431  cdom 8983  Fincfn 8985  t crest 17465  Topctop 22899  Compccmp 23394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-1o 8506  df-en 8986  df-dom 8987  df-fin 8989  df-fi 9451  df-rest 17467  df-topgen 17488  df-top 22900  df-topon 22917  df-bases 22953  df-cmp 23395
This theorem is referenced by:  cmpcld  23410  uncmp  23411  hauscmplem  23414  1stckgenlem  23561  icccmp  24847  bndth  24990  ovolicc2  25557  stoweidlem50  46065  stoweidlem57  46072
  Copyright terms: Public domain W3C validator