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

Theorem cmpsub 22751
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 2736 . . . 4 (𝐽t 𝑆) = (𝐽t 𝑆)
21iscmp 22739 . . 3 ((𝐽t 𝑆) ∈ Comp ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
3 id 22 . . . . . 6 (𝑆𝑋𝑆𝑋)
4 cmpsub.1 . . . . . . 7 𝑋 = 𝐽
54topopn 22255 . . . . . 6 (𝐽 ∈ Top → 𝑋𝐽)
6 ssexg 5280 . . . . . 6 ((𝑆𝑋𝑋𝐽) → 𝑆 ∈ V)
73, 5, 6syl2anr 597 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
8 resttop 22511 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽t 𝑆) ∈ Top)
97, 8syldan 591 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝐽t 𝑆) ∈ Top)
10 ibar 529 . . . . 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 282 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
14 vex 3449 . . . . . . . . . . 11 𝑡 ∈ V
15 eqeq1 2740 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 = (𝑦𝑆) ↔ 𝑡 = (𝑦𝑆)))
1615rexbidv 3175 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆)))
1714, 16elab 3630 . . . . . . . . . 10 (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆))
18 velpw 4565 . . . . . . . . . . . . . 14 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
19 ssel2 3939 . . . . . . . . . . . . . . . 16 ((𝑐𝐽𝑦𝑐) → 𝑦𝐽)
20 ineq1 4165 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑦 → (𝑑𝑆) = (𝑦𝑆))
2120rspceeqv 3595 . . . . . . . . . . . . . . . . 17 ((𝑦𝐽𝑡 = (𝑦𝑆)) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))
2221ex 413 . . . . . . . . . . . . . . . 16 (𝑦𝐽 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((𝑐𝐽𝑦𝑐) → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2423ex 413 . . . . . . . . . . . . . 14 (𝑐𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2518, 24sylbi 216 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2625adantl 482 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2726rexlimdv 3150 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
28 simpll 765 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
294sseq2i 3973 . . . . . . . . . . . . . 14 (𝑆𝑋𝑆 𝐽)
30 uniexg 7677 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → 𝐽 ∈ V)
31 ssexg 5280 . . . . . . . . . . . . . . . 16 ((𝑆 𝐽 𝐽 ∈ V) → 𝑆 ∈ V)
3230, 31sylan2 593 . . . . . . . . . . . . . . 15 ((𝑆 𝐽𝐽 ∈ Top) → 𝑆 ∈ V)
3332ancoms 459 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → 𝑆 ∈ V)
3429, 33sylan2b 594 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
3534adantr 481 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V)
36 elrest 17309 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3728, 35, 36syl2anc 584 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3827, 37sylibrd 258 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → 𝑡 ∈ (𝐽t 𝑆)))
3917, 38biimtrid 241 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑡 ∈ (𝐽t 𝑆)))
4039ssrdv 3950 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
41 vex 3449 . . . . . . . . . 10 𝑐 ∈ V
4241abrexex 7895 . . . . . . . . 9 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ V
4342elpw 4564 . . . . . . . 8 ({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ↔ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
4440, 43sylibr 233 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆))
45 unieq 4876 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4645eqeq2d 2747 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ( (𝐽t 𝑆) = 𝑠 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
47 pweq 4574 . . . . . . . . . . 11 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4847ineq1d 4171 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin))
4948rexeqdv 3314 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5046, 49imbi12d 344 . . . . . . . 8 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
5150rspcva 3579 . . . . . . 7 (({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5244, 51sylan 580 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5352ex 413 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
544restuni 22513 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 = (𝐽t 𝑆))
5554ad2antrr 724 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = (𝐽t 𝑆))
56 vex 3449 . . . . . . . . . . . . . 14 𝑦 ∈ V
5756inex1 5274 . . . . . . . . . . . . 13 (𝑦𝑆) ∈ V
5857dfiun2 4993 . . . . . . . . . . . 12 𝑦𝑐 (𝑦𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}
59 incom 4161 . . . . . . . . . . . . . 14 (𝑦𝑆) = (𝑆𝑦)
6059a1i 11 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑦𝑐) → (𝑦𝑆) = (𝑆𝑦))
6160iuneq2dv 4978 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑦𝑆) = 𝑦𝑐 (𝑆𝑦))
6258, 61eqtr3id 2790 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} = 𝑦𝑐 (𝑆𝑦))
63 iunin2 5031 . . . . . . . . . . . 12 𝑦𝑐 (𝑆𝑦) = (𝑆 𝑦𝑐 𝑦)
64 uniiun 5018 . . . . . . . . . . . . . . . 16 𝑐 = 𝑦𝑐 𝑦
6564eqcomi 2745 . . . . . . . . . . . . . . 15 𝑦𝑐 𝑦 = 𝑐
6665a1i 11 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 𝑦 = 𝑐)
6766ineq2d 4172 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = (𝑆 𝑐))
68 incom 4161 . . . . . . . . . . . . . . 15 (𝑆 𝑐) = ( 𝑐𝑆)
69 sseqin2 4175 . . . . . . . . . . . . . . . 16 (𝑆 𝑐 ↔ ( 𝑐𝑆) = 𝑆)
7069biimpi 215 . . . . . . . . . . . . . . 15 (𝑆 𝑐 → ( 𝑐𝑆) = 𝑆)
7168, 70eqtrid 2788 . . . . . . . . . . . . . 14 (𝑆 𝑐 → (𝑆 𝑐) = 𝑆)
7271adantl 482 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑐) = 𝑆)
7367, 72eqtrd 2776 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = 𝑆)
7463, 73eqtrid 2788 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑆𝑦) = 𝑆)
7562, 74eqtr2d 2777 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
7655, 75eqeq12d 2752 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑆 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
7755eqeq1d 2738 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑡 (𝐽t 𝑆) = 𝑡))
7877rexbidv 3175 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
7976, 78imbi12d 344 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
80 eqid 2736 . . . . . . . . . 10 𝑆 = 𝑆
8180a1bi 362 . . . . . . . . 9 (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡))
82 elin 3926 . . . . . . . . . . . 12 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin))
83 velpw 4565 . . . . . . . . . . . . . 14 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
84 dfss3 3932 . . . . . . . . . . . . . 14 (𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
85 vex 3449 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
86 eqeq1 2740 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (𝑥 = (𝑦𝑆) ↔ 𝑠 = (𝑦𝑆)))
8786rexbidv 3175 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑠 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆)))
8885, 87elab 3630 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆))
8988ralbii 3096 . . . . . . . . . . . . . 14 (∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9083, 84, 893bitri 296 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9190anbi1i 624 . . . . . . . . . . . 12 ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
9282, 91bitri 274 . . . . . . . . . . 11 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
93 ineq1 4165 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑓𝑠) → (𝑦𝑆) = ((𝑓𝑠) ∩ 𝑆))
9493eqeq2d 2747 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝑠) → (𝑠 = (𝑦𝑆) ↔ 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9594ac6sfi 9231 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9695ancoms 459 . . . . . . . . . . . . 13 ((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9796adantl 482 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
98 frn 6675 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑡𝑐 → ran 𝑓𝑐)
9998ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑐)
100 vex 3449 . . . . . . . . . . . . . . . . . . . . . 22 𝑓 ∈ V
101100rnex 7849 . . . . . . . . . . . . . . . . . . . . 21 ran 𝑓 ∈ V
102101elpw 4564 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐)
10399, 102sylibr 233 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐)
104 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin)
105104ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin)
106 ffn 6668 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑡𝑐𝑓 Fn 𝑡)
107 dffn4 6762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑡𝑓:𝑡onto→ran 𝑓)
108106, 107sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝑡𝑐𝑓:𝑡onto→ran 𝑓)
109 fodomfi 9269 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ Fin ∧ 𝑓:𝑡onto→ran 𝑓) → ran 𝑓𝑡)
110108, 109sylan2 593 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ Fin ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
111110adantll 712 . . . . . . . . . . . . . . . . . . . . . 22 (((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
112111adantll 712 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
113112ad2ant2r 745 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑡)
114 domfi 9136 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ran 𝑓𝑡) → ran 𝑓 ∈ Fin)
115105, 113, 114syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
116103, 115elind 4154 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
117 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢𝑠 = 𝑢)
118 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = 𝑢 → (𝑓𝑠) = (𝑓𝑢))
119118ineq1d 4171 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢 → ((𝑓𝑠) ∩ 𝑆) = ((𝑓𝑢) ∩ 𝑆))
120117, 119eqeq12d 2752 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑢 → (𝑠 = ((𝑓𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
121120rspccv 3578 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆) → (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)))
122 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
123 inss1 4188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)
124 sseq1 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓𝑢) ↔ ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)))
125123, 124mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓𝑢))
126 ssel 3937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢𝑤 ∈ (𝑓𝑢)))
127126a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
128125, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
129128a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))))
1301293imp 1111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))
131 fnfvelrn 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓 Fn 𝑡𝑢𝑡) → (𝑓𝑢) ∈ ran 𝑓)
132131expcom 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢𝑡 → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
1331323ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
134106, 133syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑓𝑢) ∈ ran 𝑓))
135130, 134jcad 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
1361353exp 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
137122, 136syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
138137com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑢 → (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
139138imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤𝑢𝑢𝑡) → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
140139com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
141140impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑡𝑐 ∧ (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆))) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
142121, 141sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
143 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓𝑢) ∈ V
144 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑤𝑣𝑤 ∈ (𝑓𝑢)))
145 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓𝑢) ∈ ran 𝑓))
146144, 145anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = (𝑓𝑢) → ((𝑤𝑣𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
147143, 146spcev 3565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
148142, 147syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
149148exlimdv 1936 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (∃𝑢(𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
150 eluni 4868 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑡 ↔ ∃𝑢(𝑤𝑢𝑢𝑡))
151 eluni 4868 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ran 𝑓 ↔ ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
152149, 150, 1513imtr4g 295 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑤 𝑡𝑤 ran 𝑓))
153152ssrdv 3950 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → 𝑡 ran 𝑓)
154153adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ran 𝑓)
155 sseq1 3969 . . . . . . . . . . . . . . . . . . . 20 (𝑆 = 𝑡 → (𝑆 ran 𝑓 𝑡 ran 𝑓))
156155ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (𝑆 ran 𝑓 𝑡 ran 𝑓))
157154, 156mpbird 256 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑆 ran 𝑓)
158116, 157jca 512 . . . . . . . . . . . . . . . . 17 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))
159158ex 413 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
160159eximdv 1920 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
161160ex 413 . . . . . . . . . . . . . 14 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
162161com23 86 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
163 unieq 4876 . . . . . . . . . . . . . . . 16 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
164163sseq2d 3976 . . . . . . . . . . . . . . 15 (𝑑 = ran 𝑓 → (𝑆 𝑑𝑆 ran 𝑓))
165164rspcev 3581 . . . . . . . . . . . . . 14 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
166165exlimiv 1933 . . . . . . . . . . . . 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 3152 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17181, 170biimtrrid 242 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17279, 171sylbird 259 . . . . . . 7 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
173172ex 413 . . . . . 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 3151 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
1774cmpsublem 22750 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
178176, 177impbid 211 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
17913, 178bitrd 278 1 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  𝒫 cpw 4560   cuni 4865   ciun 4954   class class class wbr 5105  ran crn 5634   Fn wfn 6491  wf 6492  ontowfo 6494  cfv 6496  (class class class)co 7357  cdom 8881  Fincfn 8883  t crest 17302  Topctop 22242  Compccmp 22737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-fin 8887  df-fi 9347  df-rest 17304  df-topgen 17325  df-top 22243  df-topon 22260  df-bases 22296  df-cmp 22738
This theorem is referenced by:  cmpcld  22753  uncmp  22754  hauscmplem  22757  1stckgenlem  22904  icccmp  24188  bndth  24321  ovolicc2  24886  stoweidlem50  44281  stoweidlem57  44288
  Copyright terms: Public domain W3C validator