Step |
Hyp |
Ref |
Expression |
1 |
|
mrcfval.f |
⊢ 𝐹 = ( mrCls ‘ 𝐶 ) |
2 |
1
|
mrcfval |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) ) |
3 |
2
|
adantr |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝐹 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) ) |
4 |
|
sseq1 |
⊢ ( 𝑥 = 𝑈 → ( 𝑥 ⊆ 𝑠 ↔ 𝑈 ⊆ 𝑠 ) ) |
5 |
4
|
rabbidv |
⊢ ( 𝑥 = 𝑈 → { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } = { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |
6 |
5
|
inteqd |
⊢ ( 𝑥 = 𝑈 → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |
7 |
6
|
adantl |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) ∧ 𝑥 = 𝑈 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |
8 |
|
mre1cl |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 ) |
9 |
|
elpw2g |
⊢ ( 𝑋 ∈ 𝐶 → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) ) |
10 |
8 9
|
syl |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) ) |
11 |
10
|
biimpar |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ∈ 𝒫 𝑋 ) |
12 |
|
sseq2 |
⊢ ( 𝑠 = 𝑋 → ( 𝑈 ⊆ 𝑠 ↔ 𝑈 ⊆ 𝑋 ) ) |
13 |
8
|
adantr |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑋 ∈ 𝐶 ) |
14 |
|
simpr |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ⊆ 𝑋 ) |
15 |
12 13 14
|
elrabd |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑋 ∈ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |
16 |
15
|
ne0d |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ≠ ∅ ) |
17 |
|
intex |
⊢ ( { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ≠ ∅ ↔ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ∈ V ) |
18 |
16 17
|
sylib |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ∈ V ) |
19 |
3 7 11 18
|
fvmptd |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |