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

Theorem cmpsub 21423
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 2770 . . . 4 (𝐽t 𝑆) = (𝐽t 𝑆)
21iscmp 21411 . . 3 ((𝐽t 𝑆) ∈ Comp ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
3 id 22 . . . . . 6 (𝑆𝑋𝑆𝑋)
4 cmpsub.1 . . . . . . 7 𝑋 = 𝐽
54topopn 20930 . . . . . 6 (𝐽 ∈ Top → 𝑋𝐽)
6 ssexg 4935 . . . . . 6 ((𝑆𝑋𝑋𝐽) → 𝑆 ∈ V)
73, 5, 6syl2anr 576 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
8 resttop 21184 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽t 𝑆) ∈ Top)
97, 8syldan 571 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝐽t 𝑆) ∈ Top)
10 ibar 512 . . . . 5 ((𝐽t 𝑆) ∈ Top → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡))))
1110bicomd 213 . . . 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, 12syl5bb 272 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
14 vex 3352 . . . . . . . . . . 11 𝑡 ∈ V
15 eqeq1 2774 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 = (𝑦𝑆) ↔ 𝑡 = (𝑦𝑆)))
1615rexbidv 3199 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆)))
1714, 16elab 3499 . . . . . . . . . 10 (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆))
18 selpw 4302 . . . . . . . . . . . . . 14 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
19 ssel2 3745 . . . . . . . . . . . . . . . 16 ((𝑐𝐽𝑦𝑐) → 𝑦𝐽)
20 ineq1 3956 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑦 → (𝑑𝑆) = (𝑦𝑆))
2120eqeq2d 2780 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑦 → (𝑡 = (𝑑𝑆) ↔ 𝑡 = (𝑦𝑆)))
2221rspcev 3458 . . . . . . . . . . . . . . . . 17 ((𝑦𝐽𝑡 = (𝑦𝑆)) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))
2322ex 397 . . . . . . . . . . . . . . . 16 (𝑦𝐽 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2419, 23syl 17 . . . . . . . . . . . . . . 15 ((𝑐𝐽𝑦𝑐) → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2524ex 397 . . . . . . . . . . . . . 14 (𝑐𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2618, 25sylbi 207 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2726adantl 467 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2827rexlimdv 3177 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
29 simpll 742 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
304sseq2i 3777 . . . . . . . . . . . . . 14 (𝑆𝑋𝑆 𝐽)
31 uniexg 7101 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → 𝐽 ∈ V)
32 ssexg 4935 . . . . . . . . . . . . . . . 16 ((𝑆 𝐽 𝐽 ∈ V) → 𝑆 ∈ V)
3331, 32sylan2 572 . . . . . . . . . . . . . . 15 ((𝑆 𝐽𝐽 ∈ Top) → 𝑆 ∈ V)
3433ancoms 455 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → 𝑆 ∈ V)
3530, 34sylan2b 573 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
3635adantr 466 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V)
37 elrest 16295 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3829, 36, 37syl2anc 565 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3928, 38sylibrd 249 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → 𝑡 ∈ (𝐽t 𝑆)))
4017, 39syl5bi 232 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑡 ∈ (𝐽t 𝑆)))
4140ssrdv 3756 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
42 vex 3352 . . . . . . . . . 10 𝑐 ∈ V
4342abrexex 7287 . . . . . . . . 9 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ V
4443elpw 4301 . . . . . . . 8 ({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ↔ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
4541, 44sylibr 224 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆))
46 unieq 4580 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4746eqeq2d 2780 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ( (𝐽t 𝑆) = 𝑠 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
48 pweq 4298 . . . . . . . . . . 11 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4948ineq1d 3962 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin))
5049rexeqdv 3293 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5147, 50imbi12d 333 . . . . . . . 8 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
5251rspcva 3456 . . . . . . 7 (({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5345, 52sylan 561 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5453ex 397 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
554restuni 21186 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 = (𝐽t 𝑆))
5655ad2antrr 697 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = (𝐽t 𝑆))
57 vex 3352 . . . . . . . . . . . . . 14 𝑦 ∈ V
5857inex1 4930 . . . . . . . . . . . . 13 (𝑦𝑆) ∈ V
5958dfiun2 4686 . . . . . . . . . . . 12 𝑦𝑐 (𝑦𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}
60 incom 3954 . . . . . . . . . . . . . 14 (𝑦𝑆) = (𝑆𝑦)
6160a1i 11 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑦𝑐) → (𝑦𝑆) = (𝑆𝑦))
6261iuneq2dv 4674 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑦𝑆) = 𝑦𝑐 (𝑆𝑦))
6359, 62syl5eqr 2818 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} = 𝑦𝑐 (𝑆𝑦))
64 iunin2 4716 . . . . . . . . . . . 12 𝑦𝑐 (𝑆𝑦) = (𝑆 𝑦𝑐 𝑦)
65 uniiun 4705 . . . . . . . . . . . . . . . 16 𝑐 = 𝑦𝑐 𝑦
6665eqcomi 2779 . . . . . . . . . . . . . . 15 𝑦𝑐 𝑦 = 𝑐
6766a1i 11 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 𝑦 = 𝑐)
6867ineq2d 3963 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = (𝑆 𝑐))
69 incom 3954 . . . . . . . . . . . . . . 15 (𝑆 𝑐) = ( 𝑐𝑆)
70 sseqin2 3966 . . . . . . . . . . . . . . . 16 (𝑆 𝑐 ↔ ( 𝑐𝑆) = 𝑆)
7170biimpi 206 . . . . . . . . . . . . . . 15 (𝑆 𝑐 → ( 𝑐𝑆) = 𝑆)
7269, 71syl5eq 2816 . . . . . . . . . . . . . 14 (𝑆 𝑐 → (𝑆 𝑐) = 𝑆)
7372adantl 467 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑐) = 𝑆)
7468, 73eqtrd 2804 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = 𝑆)
7564, 74syl5eq 2816 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑆𝑦) = 𝑆)
7663, 75eqtr2d 2805 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
7756, 76eqeq12d 2785 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑆 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
7856eqeq1d 2772 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑡 (𝐽t 𝑆) = 𝑡))
7978rexbidv 3199 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
8077, 79imbi12d 333 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
81 eqid 2770 . . . . . . . . . 10 𝑆 = 𝑆
8281a1bi 351 . . . . . . . . 9 (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡))
83 elin 3945 . . . . . . . . . . . 12 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin))
84 selpw 4302 . . . . . . . . . . . . . 14 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
85 dfss3 3739 . . . . . . . . . . . . . 14 (𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
86 vex 3352 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
87 eqeq1 2774 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (𝑥 = (𝑦𝑆) ↔ 𝑠 = (𝑦𝑆)))
8887rexbidv 3199 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑠 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆)))
8986, 88elab 3499 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆))
9089ralbii 3128 . . . . . . . . . . . . . 14 (∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9184, 85, 903bitri 286 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9291anbi1i 602 . . . . . . . . . . . 12 ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
9383, 92bitri 264 . . . . . . . . . . 11 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
94 ineq1 3956 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑓𝑠) → (𝑦𝑆) = ((𝑓𝑠) ∩ 𝑆))
9594eqeq2d 2780 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝑠) → (𝑠 = (𝑦𝑆) ↔ 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9695ac6sfi 8359 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9796ancoms 455 . . . . . . . . . . . . 13 ((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9897adantl 467 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
99 frn 6193 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑡𝑐 → ran 𝑓𝑐)
10099ad2antrl 699 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑐)
101 vex 3352 . . . . . . . . . . . . . . . . . . . . . 22 𝑓 ∈ V
102101rnex 7246 . . . . . . . . . . . . . . . . . . . . 21 ran 𝑓 ∈ V
103102elpw 4301 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐)
104100, 103sylibr 224 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐)
105 simprr 748 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin)
106105ad2antrr 697 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin)
107 ffn 6185 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑡𝑐𝑓 Fn 𝑡)
108 dffn4 6262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑡𝑓:𝑡onto→ran 𝑓)
109107, 108sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝑡𝑐𝑓:𝑡onto→ran 𝑓)
110 fodomfi 8394 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ Fin ∧ 𝑓:𝑡onto→ran 𝑓) → ran 𝑓𝑡)
111109, 110sylan2 572 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ Fin ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
112111adantll 685 . . . . . . . . . . . . . . . . . . . . . 22 (((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
113112adantll 685 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
114113ad2ant2r 733 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑡)
115 domfi 8336 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ran 𝑓𝑡) → ran 𝑓 ∈ Fin)
116106, 114, 115syl2anc 565 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
117104, 116elind 3947 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
118 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢𝑠 = 𝑢)
119 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = 𝑢 → (𝑓𝑠) = (𝑓𝑢))
120119ineq1d 3962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢 → ((𝑓𝑠) ∩ 𝑆) = ((𝑓𝑢) ∩ 𝑆))
121118, 120eqeq12d 2785 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑢 → (𝑠 = ((𝑓𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
122121rspccv 3455 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆) → (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)))
123 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
124 inss1 3979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)
125 sseq1 3773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓𝑢) ↔ ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)))
126124, 125mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓𝑢))
127 ssel 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢𝑤 ∈ (𝑓𝑢)))
128127a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
129126, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
130129a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))))
1311303imp 1100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))
132 fnfvelrn 6499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓 Fn 𝑡𝑢𝑡) → (𝑓𝑢) ∈ ran 𝑓)
133132expcom 398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢𝑡 → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
1341333ad2ant1 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
135107, 134syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑓𝑢) ∈ ran 𝑓))
136131, 135jcad 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
1371363exp 1111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
138123, 137syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
139138com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑢 → (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
140139imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤𝑢𝑢𝑡) → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
141140com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
142141impcom 394 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑡𝑐 ∧ (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆))) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
143122, 142sylan2 572 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
144 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓𝑢) ∈ V
145 eleq2 2838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑤𝑣𝑤 ∈ (𝑓𝑢)))
146 eleq1 2837 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓𝑢) ∈ ran 𝑓))
147145, 146anbi12d 608 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = (𝑓𝑢) → ((𝑤𝑣𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
148144, 147spcev 3449 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
149143, 148syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
150149exlimdv 2012 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (∃𝑢(𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
151 eluni 4575 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑡 ↔ ∃𝑢(𝑤𝑢𝑢𝑡))
152 eluni 4575 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ran 𝑓 ↔ ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
153150, 151, 1523imtr4g 285 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑤 𝑡𝑤 ran 𝑓))
154153ssrdv 3756 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → 𝑡 ran 𝑓)
155154adantl 467 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ran 𝑓)
156 sseq1 3773 . . . . . . . . . . . . . . . . . . . 20 (𝑆 = 𝑡 → (𝑆 ran 𝑓 𝑡 ran 𝑓))
157156ad2antlr 698 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (𝑆 ran 𝑓 𝑡 ran 𝑓))
158155, 157mpbird 247 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑆 ran 𝑓)
159117, 158jca 495 . . . . . . . . . . . . . . . . 17 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))
160159ex 397 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
161160eximdv 1997 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
162161ex 397 . . . . . . . . . . . . . 14 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
163162com23 86 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
164 unieq 4580 . . . . . . . . . . . . . . . 16 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
165164sseq2d 3780 . . . . . . . . . . . . . . 15 (𝑑 = ran 𝑓 → (𝑆 𝑑𝑆 ran 𝑓))
166165rspcev 3458 . . . . . . . . . . . . . 14 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
167166exlimiv 2009 . . . . . . . . . . . . 13 (∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
168163, 167syl8 76 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
16998, 168mpd 15 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17093, 169sylan2b 573 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
171170rexlimdva 3178 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17282, 171syl5bir 233 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17380, 172sylbird 250 . . . . . . 7 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
174173ex 397 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑆 𝑐 → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
175174com23 86 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → (𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
17654, 175syld 47 . . . 4 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → (𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
177176ralrimdva 3117 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
1784cmpsublem 21422 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
179177, 178impbid 202 . 2 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
18013, 179bitrd 268 1 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1070   = wceq 1630  wex 1851  wcel 2144  {cab 2756  wral 3060  wrex 3061  Vcvv 3349  cin 3720  wss 3721  𝒫 cpw 4295   cuni 4572   ciun 4652   class class class wbr 4784  ran crn 5250   Fn wfn 6026  wf 6027  ontowfo 6029  cfv 6031  (class class class)co 6792  cdom 8106  Fincfn 8108  t crest 16288  Topctop 20917  Compccmp 21409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-oadd 7716  df-er 7895  df-en 8109  df-dom 8110  df-fin 8112  df-fi 8472  df-rest 16290  df-topgen 16311  df-top 20918  df-topon 20935  df-bases 20970  df-cmp 21410
This theorem is referenced by:  cmpcld  21425  uncmp  21426  hauscmplem  21429  1stckgenlem  21576  icccmp  22847  bndth  22976  ovolicc2  23509  stoweidlem50  40778  stoweidlem57  40785
  Copyright terms: Public domain W3C validator