Step |
Hyp |
Ref |
Expression |
1 |
|
cmpsub.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
eqid |
⊢ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ ( 𝐽 ↾t 𝑆 ) |
3 |
2
|
iscmp |
⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
4 |
|
id |
⊢ ( 𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋 ) |
5 |
1
|
topopn |
⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 ) |
6 |
|
ssexg |
⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽 ) → 𝑆 ∈ V ) |
7 |
4 5 6
|
syl2anr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ V ) |
8 |
|
resttop |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐽 ↾t 𝑆 ) ∈ Top ) |
9 |
7 8
|
syldan |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Top ) |
10 |
|
ibar |
⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ Top → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ↔ ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) ) |
11 |
10
|
bicomd |
⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ Top → ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
12 |
9 11
|
syl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
13 |
3 12
|
syl5bb |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
14 |
|
vex |
⊢ 𝑡 ∈ V |
15 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑡 → ( 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ 𝑡 = ( 𝑦 ∩ 𝑆 ) ) ) |
16 |
15
|
rexbidv |
⊢ ( 𝑥 = 𝑡 → ( ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) ) ) |
17 |
14 16
|
elab |
⊢ ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) ) |
18 |
|
velpw |
⊢ ( 𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽 ) |
19 |
|
ssel2 |
⊢ ( ( 𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐 ) → 𝑦 ∈ 𝐽 ) |
20 |
|
ineq1 |
⊢ ( 𝑑 = 𝑦 → ( 𝑑 ∩ 𝑆 ) = ( 𝑦 ∩ 𝑆 ) ) |
21 |
20
|
rspceeqv |
⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝑡 = ( 𝑦 ∩ 𝑆 ) ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) |
22 |
21
|
ex |
⊢ ( 𝑦 ∈ 𝐽 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) |
23 |
19 22
|
syl |
⊢ ( ( 𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐 ) → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) |
24 |
23
|
ex |
⊢ ( 𝑐 ⊆ 𝐽 → ( 𝑦 ∈ 𝑐 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) ) |
25 |
18 24
|
sylbi |
⊢ ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑦 ∈ 𝑐 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) ) |
26 |
25
|
adantl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑦 ∈ 𝑐 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) ) |
27 |
26
|
rexlimdv |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) |
28 |
|
simpll |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → 𝐽 ∈ Top ) |
29 |
1
|
sseq2i |
⊢ ( 𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽 ) |
30 |
|
uniexg |
⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V ) |
31 |
|
ssexg |
⊢ ( ( 𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V ) → 𝑆 ∈ V ) |
32 |
30 31
|
sylan2 |
⊢ ( ( 𝑆 ⊆ ∪ 𝐽 ∧ 𝐽 ∈ Top ) → 𝑆 ∈ V ) |
33 |
32
|
ancoms |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ∈ V ) |
34 |
29 33
|
sylan2b |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ V ) |
35 |
34
|
adantr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → 𝑆 ∈ V ) |
36 |
|
elrest |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ↔ ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) |
37 |
28 35 36
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ↔ ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) |
38 |
27 37
|
sylibrd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) → 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ) ) |
39 |
17 38
|
syl5bi |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ) ) |
40 |
39
|
ssrdv |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ⊆ ( 𝐽 ↾t 𝑆 ) ) |
41 |
|
vex |
⊢ 𝑐 ∈ V |
42 |
41
|
abrexex |
⊢ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ V |
43 |
42
|
elpw |
⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ↔ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ⊆ ( 𝐽 ↾t 𝑆 ) ) |
44 |
40 43
|
sylibr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) |
45 |
|
unieq |
⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∪ 𝑠 = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) |
46 |
45
|
eqeq2d |
⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 ↔ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) ) |
47 |
|
pweq |
⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → 𝒫 𝑠 = 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) |
48 |
47
|
ineq1d |
⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ) |
49 |
48
|
rexeqdv |
⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ↔ ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) |
50 |
46 49
|
imbi12d |
⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ↔ ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
51 |
50
|
rspcva |
⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) |
52 |
44 51
|
sylan |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) |
53 |
52
|
ex |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
54 |
1
|
restuni |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) ) |
55 |
54
|
ad2antrr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) ) |
56 |
|
vex |
⊢ 𝑦 ∈ V |
57 |
56
|
inex1 |
⊢ ( 𝑦 ∩ 𝑆 ) ∈ V |
58 |
57
|
dfiun2 |
⊢ ∪ 𝑦 ∈ 𝑐 ( 𝑦 ∩ 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } |
59 |
|
incom |
⊢ ( 𝑦 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑦 ) |
60 |
59
|
a1i |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ 𝑦 ∈ 𝑐 ) → ( 𝑦 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑦 ) ) |
61 |
60
|
iuneq2dv |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ 𝑦 ∈ 𝑐 ( 𝑦 ∩ 𝑆 ) = ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) ) |
62 |
58 61
|
syl5eqr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } = ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) ) |
63 |
|
iunin2 |
⊢ ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) = ( 𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦 ) |
64 |
|
uniiun |
⊢ ∪ 𝑐 = ∪ 𝑦 ∈ 𝑐 𝑦 |
65 |
64
|
eqcomi |
⊢ ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐 |
66 |
65
|
a1i |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐 ) |
67 |
66
|
ineq2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦 ) = ( 𝑆 ∩ ∪ 𝑐 ) ) |
68 |
|
incom |
⊢ ( 𝑆 ∩ ∪ 𝑐 ) = ( ∪ 𝑐 ∩ 𝑆 ) |
69 |
|
sseqin2 |
⊢ ( 𝑆 ⊆ ∪ 𝑐 ↔ ( ∪ 𝑐 ∩ 𝑆 ) = 𝑆 ) |
70 |
69
|
biimpi |
⊢ ( 𝑆 ⊆ ∪ 𝑐 → ( ∪ 𝑐 ∩ 𝑆 ) = 𝑆 ) |
71 |
68 70
|
syl5eq |
⊢ ( 𝑆 ⊆ ∪ 𝑐 → ( 𝑆 ∩ ∪ 𝑐 ) = 𝑆 ) |
72 |
71
|
adantl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 ∩ ∪ 𝑐 ) = 𝑆 ) |
73 |
67 72
|
eqtrd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦 ) = 𝑆 ) |
74 |
63 73
|
syl5eq |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) = 𝑆 ) |
75 |
62 74
|
eqtr2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → 𝑆 = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) |
76 |
55 75
|
eqeq12d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 = 𝑆 ↔ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) ) |
77 |
55
|
eqeq1d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 = ∪ 𝑡 ↔ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) |
78 |
77
|
rexbidv |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ↔ ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) |
79 |
76 78
|
imbi12d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ) ↔ ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
80 |
|
eqid |
⊢ 𝑆 = 𝑆 |
81 |
80
|
a1bi |
⊢ ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ↔ ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ) ) |
82 |
|
elin |
⊢ ( 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ↔ ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∧ 𝑡 ∈ Fin ) ) |
83 |
|
velpw |
⊢ ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ 𝑡 ⊆ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) |
84 |
|
dfss3 |
⊢ ( 𝑡 ⊆ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∀ 𝑠 ∈ 𝑡 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) |
85 |
|
vex |
⊢ 𝑠 ∈ V |
86 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑠 → ( 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ 𝑠 = ( 𝑦 ∩ 𝑆 ) ) ) |
87 |
86
|
rexbidv |
⊢ ( 𝑥 = 𝑠 → ( ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ) ) |
88 |
85 87
|
elab |
⊢ ( 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ) |
89 |
88
|
ralbii |
⊢ ( ∀ 𝑠 ∈ 𝑡 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ) |
90 |
83 84 89
|
3bitri |
⊢ ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ) |
91 |
90
|
anbi1i |
⊢ ( ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∧ 𝑡 ∈ Fin ) ↔ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) |
92 |
82 91
|
bitri |
⊢ ( 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ↔ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) |
93 |
|
ineq1 |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑠 ) → ( 𝑦 ∩ 𝑆 ) = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) |
94 |
93
|
eqeq2d |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑠 ) → ( 𝑠 = ( 𝑦 ∩ 𝑆 ) ↔ 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) |
95 |
94
|
ac6sfi |
⊢ ( ( 𝑡 ∈ Fin ∧ ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) |
96 |
95
|
ancoms |
⊢ ( ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) |
97 |
96
|
adantl |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) |
98 |
|
frn |
⊢ ( 𝑓 : 𝑡 ⟶ 𝑐 → ran 𝑓 ⊆ 𝑐 ) |
99 |
98
|
ad2antrl |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ⊆ 𝑐 ) |
100 |
|
vex |
⊢ 𝑓 ∈ V |
101 |
100
|
rnex |
⊢ ran 𝑓 ∈ V |
102 |
101
|
elpw |
⊢ ( ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐 ) |
103 |
99 102
|
sylibr |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ 𝒫 𝑐 ) |
104 |
|
simprr |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → 𝑡 ∈ Fin ) |
105 |
104
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → 𝑡 ∈ Fin ) |
106 |
|
ffn |
⊢ ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑓 Fn 𝑡 ) |
107 |
|
dffn4 |
⊢ ( 𝑓 Fn 𝑡 ↔ 𝑓 : 𝑡 –onto→ ran 𝑓 ) |
108 |
106 107
|
sylib |
⊢ ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑓 : 𝑡 –onto→ ran 𝑓 ) |
109 |
|
fodomfi |
⊢ ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡 –onto→ ran 𝑓 ) → ran 𝑓 ≼ 𝑡 ) |
110 |
108 109
|
sylan2 |
⊢ ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡 ⟶ 𝑐 ) → ran 𝑓 ≼ 𝑡 ) |
111 |
110
|
adantll |
⊢ ( ( ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ∧ 𝑓 : 𝑡 ⟶ 𝑐 ) → ran 𝑓 ≼ 𝑡 ) |
112 |
111
|
adantll |
⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑓 : 𝑡 ⟶ 𝑐 ) → ran 𝑓 ≼ 𝑡 ) |
113 |
112
|
ad2ant2r |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ≼ 𝑡 ) |
114 |
|
domfi |
⊢ ( ( 𝑡 ∈ Fin ∧ ran 𝑓 ≼ 𝑡 ) → ran 𝑓 ∈ Fin ) |
115 |
105 113 114
|
syl2anc |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ Fin ) |
116 |
103 115
|
elind |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ) |
117 |
|
id |
⊢ ( 𝑠 = 𝑢 → 𝑠 = 𝑢 ) |
118 |
|
fveq2 |
⊢ ( 𝑠 = 𝑢 → ( 𝑓 ‘ 𝑠 ) = ( 𝑓 ‘ 𝑢 ) ) |
119 |
118
|
ineq1d |
⊢ ( 𝑠 = 𝑢 → ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) |
120 |
117 119
|
eqeq12d |
⊢ ( 𝑠 = 𝑢 → ( 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ↔ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) ) |
121 |
120
|
rspccv |
⊢ ( ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) → ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) ) |
122 |
|
pm2.27 |
⊢ ( 𝑢 ∈ 𝑡 → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) ) |
123 |
|
inss1 |
⊢ ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ⊆ ( 𝑓 ‘ 𝑢 ) |
124 |
|
sseq1 |
⊢ ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ↔ ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ⊆ ( 𝑓 ‘ 𝑢 ) ) ) |
125 |
123 124
|
mpbiri |
⊢ ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) |
126 |
|
ssel |
⊢ ( 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) → ( 𝑤 ∈ 𝑢 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) |
127 |
126
|
a1dd |
⊢ ( 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) ) |
128 |
125 127
|
syl |
⊢ ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) ) |
129 |
128
|
a1i |
⊢ ( 𝑢 ∈ 𝑡 → ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) ) ) |
130 |
129
|
3imp |
⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) |
131 |
|
fnfvelrn |
⊢ ( ( 𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) |
132 |
131
|
expcom |
⊢ ( 𝑢 ∈ 𝑡 → ( 𝑓 Fn 𝑡 → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) |
133 |
132
|
3ad2ant1 |
⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 Fn 𝑡 → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) |
134 |
106 133
|
syl5 |
⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) |
135 |
130 134
|
jcad |
⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) |
136 |
135
|
3exp |
⊢ ( 𝑢 ∈ 𝑡 → ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) ) |
137 |
122 136
|
syld |
⊢ ( 𝑢 ∈ 𝑡 → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) ) |
138 |
137
|
com3r |
⊢ ( 𝑤 ∈ 𝑢 → ( 𝑢 ∈ 𝑡 → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) ) |
139 |
138
|
imp |
⊢ ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) |
140 |
139
|
com3l |
⊢ ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) |
141 |
140
|
impcom |
⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) ) → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) |
142 |
121 141
|
sylan2 |
⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) |
143 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑢 ) ∈ V |
144 |
|
eleq2 |
⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝑤 ∈ 𝑣 ↔ 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) |
145 |
|
eleq1 |
⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝑣 ∈ ran 𝑓 ↔ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) |
146 |
144 145
|
anbi12d |
⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ↔ ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) |
147 |
143 146
|
spcev |
⊢ ( ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) → ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ) |
148 |
142 147
|
syl6 |
⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ) ) |
149 |
148
|
exlimdv |
⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ∃ 𝑢 ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ) ) |
150 |
|
eluni |
⊢ ( 𝑤 ∈ ∪ 𝑡 ↔ ∃ 𝑢 ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) ) |
151 |
|
eluni |
⊢ ( 𝑤 ∈ ∪ ran 𝑓 ↔ ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ) |
152 |
149 150 151
|
3imtr4g |
⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( 𝑤 ∈ ∪ 𝑡 → 𝑤 ∈ ∪ ran 𝑓 ) ) |
153 |
152
|
ssrdv |
⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ∪ 𝑡 ⊆ ∪ ran 𝑓 ) |
154 |
153
|
adantl |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ∪ 𝑡 ⊆ ∪ ran 𝑓 ) |
155 |
|
sseq1 |
⊢ ( 𝑆 = ∪ 𝑡 → ( 𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓 ) ) |
156 |
155
|
ad2antlr |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ( 𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓 ) ) |
157 |
154 156
|
mpbird |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → 𝑆 ⊆ ∪ ran 𝑓 ) |
158 |
116 157
|
jca |
⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) |
159 |
158
|
ex |
⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) → ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) ) |
160 |
159
|
eximdv |
⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) ) |
161 |
160
|
ex |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( 𝑆 = ∪ 𝑡 → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) ) ) |
162 |
161
|
com23 |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) ) ) |
163 |
|
unieq |
⊢ ( 𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓 ) |
164 |
163
|
sseq2d |
⊢ ( 𝑑 = ran 𝑓 → ( 𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 ⊆ ∪ ran 𝑓 ) ) |
165 |
164
|
rspcev |
⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) |
166 |
165
|
exlimiv |
⊢ ( ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) |
167 |
162 166
|
syl8 |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) ) |
168 |
97 167
|
mpd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) |
169 |
92 168
|
sylan2b |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) |
170 |
169
|
rexlimdva |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) |
171 |
81 170
|
syl5bir |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) |
172 |
79 171
|
sylbird |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) |
173 |
172
|
ex |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑆 ⊆ ∪ 𝑐 → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) ) |
174 |
173
|
com23 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) ) |
175 |
53 174
|
syld |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) ) |
176 |
175
|
ralrimdva |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) ) |
177 |
1
|
cmpsublem |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) |
178 |
176 177
|
impbid |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) ) |
179 |
13 178
|
bitrd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) ) |