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

Theorem cmpsub 22904
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 2733 . . . 4 (𝐽t 𝑆) = (𝐽t 𝑆)
21iscmp 22892 . . 3 ((𝐽t 𝑆) ∈ Comp ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
3 id 22 . . . . . 6 (𝑆𝑋𝑆𝑋)
4 cmpsub.1 . . . . . . 7 𝑋 = 𝐽
54topopn 22408 . . . . . 6 (𝐽 ∈ Top → 𝑋𝐽)
6 ssexg 5324 . . . . . 6 ((𝑆𝑋𝑋𝐽) → 𝑆 ∈ V)
73, 5, 6syl2anr 598 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
8 resttop 22664 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽t 𝑆) ∈ Top)
97, 8syldan 592 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝐽t 𝑆) ∈ Top)
10 ibar 530 . . . . 5 ((𝐽t 𝑆) ∈ Top → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡))))
1110bicomd 222 . . . 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 3479 . . . . . . . . . . 11 𝑡 ∈ V
15 eqeq1 2737 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 = (𝑦𝑆) ↔ 𝑡 = (𝑦𝑆)))
1615rexbidv 3179 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆)))
1714, 16elab 3669 . . . . . . . . . 10 (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆))
18 velpw 4608 . . . . . . . . . . . . . 14 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
19 ssel2 3978 . . . . . . . . . . . . . . . 16 ((𝑐𝐽𝑦𝑐) → 𝑦𝐽)
20 ineq1 4206 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑦 → (𝑑𝑆) = (𝑦𝑆))
2120rspceeqv 3634 . . . . . . . . . . . . . . . . 17 ((𝑦𝐽𝑡 = (𝑦𝑆)) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))
2221ex 414 . . . . . . . . . . . . . . . 16 (𝑦𝐽 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((𝑐𝐽𝑦𝑐) → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2423ex 414 . . . . . . . . . . . . . 14 (𝑐𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2518, 24sylbi 216 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2625adantl 483 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2726rexlimdv 3154 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
28 simpll 766 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
294sseq2i 4012 . . . . . . . . . . . . . 14 (𝑆𝑋𝑆 𝐽)
30 uniexg 7730 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → 𝐽 ∈ V)
31 ssexg 5324 . . . . . . . . . . . . . . . 16 ((𝑆 𝐽 𝐽 ∈ V) → 𝑆 ∈ V)
3230, 31sylan2 594 . . . . . . . . . . . . . . 15 ((𝑆 𝐽𝐽 ∈ Top) → 𝑆 ∈ V)
3332ancoms 460 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → 𝑆 ∈ V)
3429, 33sylan2b 595 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
3534adantr 482 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V)
36 elrest 17373 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3728, 35, 36syl2anc 585 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3827, 37sylibrd 259 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → 𝑡 ∈ (𝐽t 𝑆)))
3917, 38biimtrid 241 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑡 ∈ (𝐽t 𝑆)))
4039ssrdv 3989 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
41 vex 3479 . . . . . . . . . 10 𝑐 ∈ V
4241abrexex 7949 . . . . . . . . 9 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ V
4342elpw 4607 . . . . . . . 8 ({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ↔ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
4440, 43sylibr 233 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆))
45 unieq 4920 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4645eqeq2d 2744 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ( (𝐽t 𝑆) = 𝑠 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
47 pweq 4617 . . . . . . . . . . 11 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4847ineq1d 4212 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin))
4948rexeqdv 3327 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5046, 49imbi12d 345 . . . . . . . 8 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
5150rspcva 3611 . . . . . . 7 (({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5244, 51sylan 581 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5352ex 414 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
544restuni 22666 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 = (𝐽t 𝑆))
5554ad2antrr 725 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = (𝐽t 𝑆))
56 vex 3479 . . . . . . . . . . . . . 14 𝑦 ∈ V
5756inex1 5318 . . . . . . . . . . . . 13 (𝑦𝑆) ∈ V
5857dfiun2 5037 . . . . . . . . . . . 12 𝑦𝑐 (𝑦𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}
59 incom 4202 . . . . . . . . . . . . . 14 (𝑦𝑆) = (𝑆𝑦)
6059a1i 11 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑦𝑐) → (𝑦𝑆) = (𝑆𝑦))
6160iuneq2dv 5022 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑦𝑆) = 𝑦𝑐 (𝑆𝑦))
6258, 61eqtr3id 2787 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} = 𝑦𝑐 (𝑆𝑦))
63 iunin2 5075 . . . . . . . . . . . 12 𝑦𝑐 (𝑆𝑦) = (𝑆 𝑦𝑐 𝑦)
64 uniiun 5062 . . . . . . . . . . . . . . . 16 𝑐 = 𝑦𝑐 𝑦
6564eqcomi 2742 . . . . . . . . . . . . . . 15 𝑦𝑐 𝑦 = 𝑐
6665a1i 11 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 𝑦 = 𝑐)
6766ineq2d 4213 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = (𝑆 𝑐))
68 incom 4202 . . . . . . . . . . . . . . 15 (𝑆 𝑐) = ( 𝑐𝑆)
69 sseqin2 4216 . . . . . . . . . . . . . . . 16 (𝑆 𝑐 ↔ ( 𝑐𝑆) = 𝑆)
7069biimpi 215 . . . . . . . . . . . . . . 15 (𝑆 𝑐 → ( 𝑐𝑆) = 𝑆)
7168, 70eqtrid 2785 . . . . . . . . . . . . . 14 (𝑆 𝑐 → (𝑆 𝑐) = 𝑆)
7271adantl 483 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑐) = 𝑆)
7367, 72eqtrd 2773 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = 𝑆)
7463, 73eqtrid 2785 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑆𝑦) = 𝑆)
7562, 74eqtr2d 2774 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
7655, 75eqeq12d 2749 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑆 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
7755eqeq1d 2735 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑡 (𝐽t 𝑆) = 𝑡))
7877rexbidv 3179 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
7976, 78imbi12d 345 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
80 eqid 2733 . . . . . . . . . 10 𝑆 = 𝑆
8180a1bi 363 . . . . . . . . 9 (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡))
82 elin 3965 . . . . . . . . . . . 12 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin))
83 velpw 4608 . . . . . . . . . . . . . 14 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
84 dfss3 3971 . . . . . . . . . . . . . 14 (𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
85 vex 3479 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
86 eqeq1 2737 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (𝑥 = (𝑦𝑆) ↔ 𝑠 = (𝑦𝑆)))
8786rexbidv 3179 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑠 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆)))
8885, 87elab 3669 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆))
8988ralbii 3094 . . . . . . . . . . . . . 14 (∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9083, 84, 893bitri 297 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9190anbi1i 625 . . . . . . . . . . . 12 ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
9282, 91bitri 275 . . . . . . . . . . 11 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
93 ineq1 4206 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑓𝑠) → (𝑦𝑆) = ((𝑓𝑠) ∩ 𝑆))
9493eqeq2d 2744 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝑠) → (𝑠 = (𝑦𝑆) ↔ 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9594ac6sfi 9287 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9695ancoms 460 . . . . . . . . . . . . 13 ((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9796adantl 483 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
98 frn 6725 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑡𝑐 → ran 𝑓𝑐)
9998ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑐)
100 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑓 ∈ V
101100rnex 7903 . . . . . . . . . . . . . . . . . . . . 21 ran 𝑓 ∈ V
102101elpw 4607 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐)
10399, 102sylibr 233 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐)
104 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin)
105104ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin)
106 ffn 6718 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑡𝑐𝑓 Fn 𝑡)
107 dffn4 6812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑡𝑓:𝑡onto→ran 𝑓)
108106, 107sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝑡𝑐𝑓:𝑡onto→ran 𝑓)
109 fodomfi 9325 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ Fin ∧ 𝑓:𝑡onto→ran 𝑓) → ran 𝑓𝑡)
110108, 109sylan2 594 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ Fin ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
111110adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 (((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
112111adantll 713 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
113112ad2ant2r 746 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑡)
114 domfi 9192 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ran 𝑓𝑡) → ran 𝑓 ∈ Fin)
115105, 113, 114syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
116103, 115elind 4195 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
117 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢𝑠 = 𝑢)
118 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = 𝑢 → (𝑓𝑠) = (𝑓𝑢))
119118ineq1d 4212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢 → ((𝑓𝑠) ∩ 𝑆) = ((𝑓𝑢) ∩ 𝑆))
120117, 119eqeq12d 2749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑢 → (𝑠 = ((𝑓𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
121120rspccv 3610 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆) → (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)))
122 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
123 inss1 4229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)
124 sseq1 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓𝑢) ↔ ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)))
125123, 124mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓𝑢))
126 ssel 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢𝑤 ∈ (𝑓𝑢)))
127126a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
128125, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
129128a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))))
1301293imp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))
131 fnfvelrn 7083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓 Fn 𝑡𝑢𝑡) → (𝑓𝑢) ∈ ran 𝑓)
132131expcom 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢𝑡 → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
1331323ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
134106, 133syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑓𝑢) ∈ ran 𝑓))
135130, 134jcad 514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
1361353exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
137122, 136syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
138137com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑢 → (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
139138imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤𝑢𝑢𝑡) → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
140139com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
141140impcom 409 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑡𝑐 ∧ (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆))) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
142121, 141sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
143 fvex 6905 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓𝑢) ∈ V
144 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑤𝑣𝑤 ∈ (𝑓𝑢)))
145 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓𝑢) ∈ ran 𝑓))
146144, 145anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = (𝑓𝑢) → ((𝑤𝑣𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
147143, 146spcev 3597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
148142, 147syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
149148exlimdv 1937 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (∃𝑢(𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
150 eluni 4912 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑡 ↔ ∃𝑢(𝑤𝑢𝑢𝑡))
151 eluni 4912 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ran 𝑓 ↔ ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
152149, 150, 1513imtr4g 296 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑤 𝑡𝑤 ran 𝑓))
153152ssrdv 3989 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → 𝑡 ran 𝑓)
154153adantl 483 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ran 𝑓)
155 sseq1 4008 . . . . . . . . . . . . . . . . . . . 20 (𝑆 = 𝑡 → (𝑆 ran 𝑓 𝑡 ran 𝑓))
156155ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (𝑆 ran 𝑓 𝑡 ran 𝑓))
157154, 156mpbird 257 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑆 ran 𝑓)
158116, 157jca 513 . . . . . . . . . . . . . . . . 17 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))
159158ex 414 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
160159eximdv 1921 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
161160ex 414 . . . . . . . . . . . . . 14 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
162161com23 86 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
163 unieq 4920 . . . . . . . . . . . . . . . 16 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
164163sseq2d 4015 . . . . . . . . . . . . . . 15 (𝑑 = ran 𝑓 → (𝑆 𝑑𝑆 ran 𝑓))
165164rspcev 3613 . . . . . . . . . . . . . 14 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
166165exlimiv 1934 . . . . . . . . . . . . 13 (∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
167162, 166syl8 76 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
16897, 167mpd 15 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
16992, 168sylan2b 595 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
170169rexlimdva 3156 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17181, 170biimtrrid 242 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17279, 171sylbird 260 . . . . . . 7 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
173172ex 414 . . . . . 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 3155 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
1774cmpsublem 22903 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
178176, 177impbid 211 . 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 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  {cab 2710  wral 3062  wrex 3071  Vcvv 3475  cin 3948  wss 3949  𝒫 cpw 4603   cuni 4909   ciun 4998   class class class wbr 5149  ran crn 5678   Fn wfn 6539  wf 6540  ontowfo 6542  cfv 6544  (class class class)co 7409  cdom 8937  Fincfn 8939  t crest 17366  Topctop 22395  Compccmp 22890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9406  df-rest 17368  df-topgen 17389  df-top 22396  df-topon 22413  df-bases 22449  df-cmp 22891
This theorem is referenced by:  cmpcld  22906  uncmp  22907  hauscmplem  22910  1stckgenlem  23057  icccmp  24341  bndth  24474  ovolicc2  25039  stoweidlem50  44766  stoweidlem57  44773
  Copyright terms: Public domain W3C validator