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

Theorem cmpsub 21126
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 2621 . . . 4 (𝐽t 𝑆) = (𝐽t 𝑆)
21iscmp 21114 . . 3 ((𝐽t 𝑆) ∈ Comp ↔ ((𝐽t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)))
3 id 22 . . . . . 6 (𝑆𝑋𝑆𝑋)
4 cmpsub.1 . . . . . . 7 𝑋 = 𝐽
54topopn 20643 . . . . . 6 (𝐽 ∈ Top → 𝑋𝐽)
6 ssexg 4769 . . . . . 6 ((𝑆𝑋𝑋𝐽) → 𝑆 ∈ V)
73, 5, 6syl2anr 495 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
8 resttop 20887 . . . . 5 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽t 𝑆) ∈ Top)
97, 8syldan 487 . . . 4 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝐽t 𝑆) ∈ Top)
10 ibar 525 . . . . 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 3192 . . . . . . . . . . 11 𝑡 ∈ V
15 eqeq1 2625 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 = (𝑦𝑆) ↔ 𝑡 = (𝑦𝑆)))
1615rexbidv 3046 . . . . . . . . . . 11 (𝑥 = 𝑡 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆)))
1714, 16elab 3337 . . . . . . . . . 10 (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑡 = (𝑦𝑆))
18 selpw 4142 . . . . . . . . . . . . . 14 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
19 ssel2 3582 . . . . . . . . . . . . . . . 16 ((𝑐𝐽𝑦𝑐) → 𝑦𝐽)
20 ineq1 3790 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑦 → (𝑑𝑆) = (𝑦𝑆))
2120eqeq2d 2631 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑦 → (𝑡 = (𝑑𝑆) ↔ 𝑡 = (𝑦𝑆)))
2221rspcev 3298 . . . . . . . . . . . . . . . . 17 ((𝑦𝐽𝑡 = (𝑦𝑆)) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))
2322ex 450 . . . . . . . . . . . . . . . 16 (𝑦𝐽 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2419, 23syl 17 . . . . . . . . . . . . . . 15 ((𝑐𝐽𝑦𝑐) → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
2524ex 450 . . . . . . . . . . . . . 14 (𝑐𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2618, 25sylbi 207 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 𝐽 → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2726adantl 482 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦𝑐 → (𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆))))
2827rexlimdv 3024 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
29 simpll 789 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
304sseq2i 3614 . . . . . . . . . . . . . 14 (𝑆𝑋𝑆 𝐽)
31 uniexg 6915 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → 𝐽 ∈ V)
32 ssexg 4769 . . . . . . . . . . . . . . . 16 ((𝑆 𝐽 𝐽 ∈ V) → 𝑆 ∈ V)
3331, 32sylan2 491 . . . . . . . . . . . . . . 15 ((𝑆 𝐽𝐽 ∈ Top) → 𝑆 ∈ V)
3433ancoms 469 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → 𝑆 ∈ V)
3530, 34sylan2b 492 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ∈ V)
3635adantr 481 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V)
37 elrest 16020 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3829, 36, 37syl2anc 692 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽t 𝑆) ↔ ∃𝑑𝐽 𝑡 = (𝑑𝑆)))
3928, 38sylibrd 249 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦𝑐 𝑡 = (𝑦𝑆) → 𝑡 ∈ (𝐽t 𝑆)))
4017, 39syl5bi 232 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑡 ∈ (𝐽t 𝑆)))
4140ssrdv 3593 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
42 vex 3192 . . . . . . . . . 10 𝑐 ∈ V
4342abrexex 7094 . . . . . . . . 9 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ V
4443elpw 4141 . . . . . . . 8 ({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ↔ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ⊆ (𝐽t 𝑆))
4541, 44sylibr 224 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆))
46 unieq 4415 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4746eqeq2d 2631 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ( (𝐽t 𝑆) = 𝑠 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
48 pweq 4138 . . . . . . . . . . 11 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
4948ineq1d 3796 . . . . . . . . . 10 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin))
5049rexeqdv 3137 . . . . . . . . 9 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5147, 50imbi12d 334 . . . . . . . 8 (𝑠 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → (( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
5251rspcva 3296 . . . . . . 7 (({𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∈ 𝒫 (𝐽t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5345, 52sylan 488 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡)) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
5453ex 450 . . . . 5 (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
554restuni 20889 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 = (𝐽t 𝑆))
5655ad2antrr 761 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = (𝐽t 𝑆))
57 vex 3192 . . . . . . . . . . . . . 14 𝑦 ∈ V
5857inex1 4764 . . . . . . . . . . . . 13 (𝑦𝑆) ∈ V
5958dfiun2 4525 . . . . . . . . . . . 12 𝑦𝑐 (𝑦𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}
60 incom 3788 . . . . . . . . . . . . . 14 (𝑦𝑆) = (𝑆𝑦)
6160a1i 11 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑦𝑐) → (𝑦𝑆) = (𝑆𝑦))
6261iuneq2dv 4513 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑦𝑆) = 𝑦𝑐 (𝑆𝑦))
6359, 62syl5eqr 2669 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} = 𝑦𝑐 (𝑆𝑦))
64 iunin2 4555 . . . . . . . . . . . 12 𝑦𝑐 (𝑆𝑦) = (𝑆 𝑦𝑐 𝑦)
65 uniiun 4544 . . . . . . . . . . . . . . . 16 𝑐 = 𝑦𝑐 𝑦
6665eqcomi 2630 . . . . . . . . . . . . . . 15 𝑦𝑐 𝑦 = 𝑐
6766a1i 11 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 𝑦 = 𝑐)
6867ineq2d 3797 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = (𝑆 𝑐))
69 incom 3788 . . . . . . . . . . . . . . 15 (𝑆 𝑐) = ( 𝑐𝑆)
70 sseqin2 3800 . . . . . . . . . . . . . . . 16 (𝑆 𝑐 ↔ ( 𝑐𝑆) = 𝑆)
7170biimpi 206 . . . . . . . . . . . . . . 15 (𝑆 𝑐 → ( 𝑐𝑆) = 𝑆)
7269, 71syl5eq 2667 . . . . . . . . . . . . . 14 (𝑆 𝑐 → (𝑆 𝑐) = 𝑆)
7372adantl 482 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑐) = 𝑆)
7468, 73eqtrd 2655 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 𝑦𝑐 𝑦) = 𝑆)
7564, 74syl5eq 2667 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑦𝑐 (𝑆𝑦) = 𝑆)
7663, 75eqtr2d 2656 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → 𝑆 = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
7756, 76eqeq12d 2636 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑆 (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)}))
7856eqeq1d 2623 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (𝑆 = 𝑡 (𝐽t 𝑆) = 𝑡))
7978rexbidv 3046 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡))
8077, 79imbi12d 334 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) ↔ ( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡)))
81 eqid 2621 . . . . . . . . . 10 𝑆 = 𝑆
8281a1bi 352 . . . . . . . . 9 (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡))
83 elin 3779 . . . . . . . . . . . 12 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin))
84 selpw 4142 . . . . . . . . . . . . . 14 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
85 dfss3 3577 . . . . . . . . . . . . . 14 (𝑡 ⊆ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)})
86 vex 3192 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
87 eqeq1 2625 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (𝑥 = (𝑦𝑆) ↔ 𝑠 = (𝑦𝑆)))
8887rexbidv 3046 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑠 → (∃𝑦𝑐 𝑥 = (𝑦𝑆) ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆)))
8986, 88elab 3337 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∃𝑦𝑐 𝑠 = (𝑦𝑆))
9089ralbii 2975 . . . . . . . . . . . . . 14 (∀𝑠𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9184, 85, 903bitri 286 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ↔ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆))
9291anbi1i 730 . . . . . . . . . . . 12 ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
9383, 92bitri 264 . . . . . . . . . . 11 (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) ↔ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin))
94 ineq1 3790 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑓𝑠) → (𝑦𝑆) = ((𝑓𝑠) ∩ 𝑆))
9594eqeq2d 2631 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝑠) → (𝑠 = (𝑦𝑆) ↔ 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9695ac6sfi 8156 . . . . . . . . . . . . . 14 ((𝑡 ∈ Fin ∧ ∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9796ancoms 469 . . . . . . . . . . . . 13 ((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
9897adantl 482 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)))
99 frn 6015 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑡𝑐 → ran 𝑓𝑐)
10099ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑐)
101 vex 3192 . . . . . . . . . . . . . . . . . . . . . 22 𝑓 ∈ V
102101rnex 7054 . . . . . . . . . . . . . . . . . . . . 21 ran 𝑓 ∈ V
103102elpw 4141 . . . . . . . . . . . . . . . . . . . 20 (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓𝑐)
104100, 103sylibr 224 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐)
105 simprr 795 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin)
106105ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin)
107 ffn 6007 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑡𝑐𝑓 Fn 𝑡)
108 dffn4 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑡𝑓:𝑡onto→ran 𝑓)
109107, 108sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝑡𝑐𝑓:𝑡onto→ran 𝑓)
110 fodomfi 8191 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ Fin ∧ 𝑓:𝑡onto→ran 𝑓) → ran 𝑓𝑡)
111109, 110sylan2 491 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ Fin ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
112111adantll 749 . . . . . . . . . . . . . . . . . . . . . 22 (((∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
113112adantll 749 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡𝑐) → ran 𝑓𝑡)
114113ad2ant2r 782 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓𝑡)
115 domfi 8133 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ Fin ∧ ran 𝑓𝑡) → ran 𝑓 ∈ Fin)
116106, 114, 115syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
117104, 116elind 3781 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
118 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢𝑠 = 𝑢)
119 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = 𝑢 → (𝑓𝑠) = (𝑓𝑢))
120119ineq1d 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = 𝑢 → ((𝑓𝑠) ∩ 𝑆) = ((𝑓𝑢) ∩ 𝑆))
121118, 120eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = 𝑢 → (𝑠 = ((𝑓𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
122121rspccv 3295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆) → (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)))
123 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓𝑢) ∩ 𝑆)))
124 inss1 3816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)
125 sseq1 3610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓𝑢) ↔ ((𝑓𝑢) ∩ 𝑆) ⊆ (𝑓𝑢)))
126124, 125mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓𝑢))
127 ssel 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢𝑤 ∈ (𝑓𝑢)))
128127a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑢 ⊆ (𝑓𝑢) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
129126, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢))))
130129a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))))
1311303imp 1254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐𝑤 ∈ (𝑓𝑢)))
132 fnfvelrn 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓 Fn 𝑡𝑢𝑡) → (𝑓𝑢) ∈ ran 𝑓)
133132expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢𝑡 → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
1341333ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓 Fn 𝑡 → (𝑓𝑢) ∈ ran 𝑓))
135107, 134syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑓𝑢) ∈ ran 𝑓))
136131, 135jcad 555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆) ∧ 𝑤𝑢) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
1371363exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢𝑡 → (𝑢 = ((𝑓𝑢) ∩ 𝑆) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
138123, 137syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑤𝑢 → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
139138com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑢 → (𝑢𝑡 → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))))
140139imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑤𝑢𝑢𝑡) → ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
141140com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆)) → (𝑓:𝑡𝑐 → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓))))
142141impcom 446 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑡𝑐 ∧ (𝑢𝑡𝑢 = ((𝑓𝑢) ∩ 𝑆))) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
143122, 142sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
144 fvex 6163 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓𝑢) ∈ V
145 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑤𝑣𝑤 ∈ (𝑓𝑢)))
146 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑓𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓𝑢) ∈ ran 𝑓))
147145, 146anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = (𝑓𝑢) → ((𝑤𝑣𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓)))
148144, 147spcev 3289 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤 ∈ (𝑓𝑢) ∧ (𝑓𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
149143, 148syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ((𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
150149exlimdv 1858 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (∃𝑢(𝑤𝑢𝑢𝑡) → ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓)))
151 eluni 4410 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 𝑡 ↔ ∃𝑢(𝑤𝑢𝑢𝑡))
152 eluni 4410 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ran 𝑓 ↔ ∃𝑣(𝑤𝑣𝑣 ∈ ran 𝑓))
153150, 151, 1523imtr4g 285 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑤 𝑡𝑤 ran 𝑓))
154153ssrdv 3593 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → 𝑡 ran 𝑓)
155154adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑡 ran 𝑓)
156 sseq1 3610 . . . . . . . . . . . . . . . . . . . 20 (𝑆 = 𝑡 → (𝑆 ran 𝑓 𝑡 ran 𝑓))
157156ad2antlr 762 . . . . . . . . . . . . . . . . . . 19 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (𝑆 ran 𝑓 𝑡 ran 𝑓))
158155, 157mpbird 247 . . . . . . . . . . . . . . . . . 18 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → 𝑆 ran 𝑓)
159117, 158jca 554 . . . . . . . . . . . . . . . . 17 (((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) ∧ (𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))
160159ex 450 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → ((𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
161160eximdv 1843 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = 𝑡) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓)))
162161ex 450 . . . . . . . . . . . . . 14 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
163162com23 86 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓))))
164 unieq 4415 . . . . . . . . . . . . . . . 16 (𝑑 = ran 𝑓 𝑑 = ran 𝑓)
165164sseq2d 3617 . . . . . . . . . . . . . . 15 (𝑑 = ran 𝑓 → (𝑆 𝑑𝑆 ran 𝑓))
166165rspcev 3298 . . . . . . . . . . . . . 14 ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
167166exlimiv 1855 . . . . . . . . . . . . 13 (∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)
168163, 167syl8 76 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡𝑐 ∧ ∀𝑠𝑡 𝑠 = ((𝑓𝑠) ∩ 𝑆)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
16998, 168mpd 15 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ (∀𝑠𝑡𝑦𝑐 𝑠 = (𝑦𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17093, 169sylan2b 492 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)) → (𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
171170rexlimdva 3025 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17282, 171syl5bir 233 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin)𝑆 = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
17380, 172sylbird 250 . . . . . . 7 ((((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 𝑐) → (( (𝐽t 𝑆) = {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦𝑐 𝑥 = (𝑦𝑆)} ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑))
174173ex 450 . . . . . 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 2964 . . 3 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (∀𝑠 ∈ 𝒫 (𝐽t 𝑆)( (𝐽t 𝑆) = 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin) (𝐽t 𝑆) = 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑑)))
1784cmpsublem 21125 . . 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 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wral 2907  wrex 2908  Vcvv 3189  cin 3558  wss 3559  𝒫 cpw 4135   cuni 4407   ciun 4490   class class class wbr 4618  ran crn 5080   Fn wfn 5847  wf 5848  ontowfo 5850  cfv 5852  (class class class)co 6610  cdom 7905  Fincfn 7907  t crest 16013  Topctop 20630  Compccmp 21112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7908  df-dom 7909  df-fin 7911  df-fi 8269  df-rest 16015  df-topgen 16036  df-top 20631  df-topon 20648  df-bases 20674  df-cmp 21113
This theorem is referenced by:  cmpcld  21128  uncmp  21129  hauscmplem  21132  1stckgenlem  21279  icccmp  22551  bndth  22680  ovolicc2  23213  stoweidlem50  39600  stoweidlem57  39607
  Copyright terms: Public domain W3C validator