| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) |
| 2 |
|
utopval |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 } ) |
| 3 |
|
ssrab2 |
⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 } ⊆ 𝒫 𝑋 |
| 4 |
2 3
|
eqsstrdi |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 ) |
| 5 |
4
|
adantr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 ) |
| 6 |
1 5
|
sstrd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → 𝑥 ⊆ 𝒫 𝑋 ) |
| 7 |
|
sspwuni |
⊢ ( 𝑥 ⊆ 𝒫 𝑋 ↔ ∪ 𝑥 ⊆ 𝑋 ) |
| 8 |
6 7
|
sylib |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∪ 𝑥 ⊆ 𝑋 ) |
| 9 |
|
simp-4l |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
| 10 |
|
simp-4r |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) |
| 11 |
|
simplr |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑦 ∈ 𝑥 ) |
| 12 |
10 11
|
sseldd |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) |
| 13 |
|
simpr |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑝 ∈ 𝑦 ) |
| 14 |
|
elutop |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑦 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑦 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑦 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) |
| 15 |
14
|
biimpa |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑦 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑦 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) |
| 16 |
15
|
simprd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ 𝑦 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) |
| 17 |
16
|
r19.21bi |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ 𝑦 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) |
| 18 |
9 12 13 17
|
syl21anc |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) |
| 19 |
|
r19.41v |
⊢ ( ∃ 𝑣 ∈ 𝑈 ( ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ↔ ( ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) |
| 20 |
|
ssuni |
⊢ ( ( ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) |
| 21 |
20
|
reximi |
⊢ ( ∃ 𝑣 ∈ 𝑈 ( ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) |
| 22 |
19 21
|
sylbir |
⊢ ( ( ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) |
| 23 |
18 11 22
|
syl2anc |
⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) |
| 24 |
|
eluni2 |
⊢ ( 𝑝 ∈ ∪ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 𝑝 ∈ 𝑦 ) |
| 25 |
24
|
biimpi |
⊢ ( 𝑝 ∈ ∪ 𝑥 → ∃ 𝑦 ∈ 𝑥 𝑝 ∈ 𝑦 ) |
| 26 |
25
|
adantl |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) → ∃ 𝑦 ∈ 𝑥 𝑝 ∈ 𝑦 ) |
| 27 |
23 26
|
r19.29a |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) |
| 28 |
27
|
ralrimiva |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) |
| 29 |
|
elutop |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) ) ) |
| 30 |
29
|
adantr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ( ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) ) ) |
| 31 |
8 28 30
|
mpbir2and |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) |
| 32 |
31
|
ex |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ) |
| 33 |
32
|
alrimiv |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ) |
| 34 |
|
elutop |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) ) ) |
| 35 |
34
|
biimpa |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) ) |
| 36 |
35
|
simpld |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → 𝑥 ⊆ 𝑋 ) |
| 37 |
36
|
adantrr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → 𝑥 ⊆ 𝑋 ) |
| 38 |
|
ssinss1 |
⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ) |
| 39 |
37 38
|
syl |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ) |
| 40 |
|
simpl |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
| 41 |
|
simpr31 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑢 ∈ 𝑈 ) |
| 42 |
|
simpr32 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑣 ∈ 𝑈 ) |
| 43 |
|
ustincl |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 ) |
| 44 |
40 41 42 43
|
syl3anc |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 ) |
| 45 |
|
inss1 |
⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢 |
| 46 |
|
imass1 |
⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢 → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑢 “ { 𝑝 } ) ) |
| 47 |
45 46
|
ax-mp |
⊢ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑢 “ { 𝑝 } ) |
| 48 |
|
simpr33 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) |
| 49 |
48
|
simpld |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) |
| 50 |
47 49
|
sstrid |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ 𝑥 ) |
| 51 |
|
inss2 |
⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣 |
| 52 |
|
imass1 |
⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣 → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑣 “ { 𝑝 } ) ) |
| 53 |
51 52
|
ax-mp |
⊢ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑣 “ { 𝑝 } ) |
| 54 |
48
|
simprd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) |
| 55 |
53 54
|
sstrid |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ 𝑦 ) |
| 56 |
50 55
|
ssind |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 57 |
|
imaeq1 |
⊢ ( 𝑤 = ( 𝑢 ∩ 𝑣 ) → ( 𝑤 “ { 𝑝 } ) = ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ) |
| 58 |
57
|
sseq1d |
⊢ ( 𝑤 = ( 𝑢 ∩ 𝑣 ) → ( ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
| 59 |
58
|
rspcev |
⊢ ( ( ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 ∧ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 60 |
44 56 59
|
syl2anc |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 61 |
60
|
3anassrs |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 62 |
61
|
3anassrs |
⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 63 |
|
simpll |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
| 64 |
|
simplrl |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) |
| 65 |
|
simpr |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) |
| 66 |
|
elin |
⊢ ( 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑝 ∈ 𝑥 ∧ 𝑝 ∈ 𝑦 ) ) |
| 67 |
65 66
|
sylib |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( 𝑝 ∈ 𝑥 ∧ 𝑝 ∈ 𝑦 ) ) |
| 68 |
67
|
simpld |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ 𝑥 ) |
| 69 |
35
|
simprd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) |
| 70 |
69
|
r19.21bi |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ 𝑥 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) |
| 71 |
63 64 68 70
|
syl21anc |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) |
| 72 |
|
simplrr |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) |
| 73 |
67
|
simprd |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ 𝑦 ) |
| 74 |
63 72 73 17
|
syl21anc |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) |
| 75 |
|
reeanv |
⊢ ( ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ↔ ( ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) |
| 76 |
71 74 75
|
sylanbrc |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) |
| 77 |
62 76
|
r19.29vva |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 78 |
77
|
ralrimiva |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 79 |
|
elutop |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 80 |
79
|
adantr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 81 |
39 78 80
|
mpbir2and |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) |
| 82 |
81
|
ralrimivva |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) |
| 83 |
|
fvex |
⊢ ( unifTop ‘ 𝑈 ) ∈ V |
| 84 |
|
istopg |
⊢ ( ( unifTop ‘ 𝑈 ) ∈ V → ( ( unifTop ‘ 𝑈 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) ) ) |
| 85 |
83 84
|
ax-mp |
⊢ ( ( unifTop ‘ 𝑈 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) ) |
| 86 |
33 82 85
|
sylanbrc |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top ) |