Step |
Hyp |
Ref |
Expression |
1 |
|
mrcfval.f |
⊢ 𝐹 = ( mrCls ‘ 𝐶 ) |
2 |
|
sstr2 |
⊢ ( 𝑈 ⊆ 𝑉 → ( 𝑉 ⊆ 𝑠 → 𝑈 ⊆ 𝑠 ) ) |
3 |
2
|
adantr |
⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑠 ∈ 𝐶 ) → ( 𝑉 ⊆ 𝑠 → 𝑈 ⊆ 𝑠 ) ) |
4 |
3
|
ss2rabdv |
⊢ ( 𝑈 ⊆ 𝑉 → { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ⊆ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |
5 |
|
intss |
⊢ ( { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ⊆ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ⊆ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ) |
6 |
4 5
|
syl |
⊢ ( 𝑈 ⊆ 𝑉 → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ⊆ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ⊆ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ) |
8 |
|
simp1 |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) ) |
9 |
|
sstr |
⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → 𝑈 ⊆ 𝑋 ) |
10 |
9
|
3adant1 |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → 𝑈 ⊆ 𝑋 ) |
11 |
1
|
mrcval |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |
12 |
8 10 11
|
syl2anc |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } ) |
13 |
1
|
mrcval |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑉 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ) |
14 |
13
|
3adant2 |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑉 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑉 ⊆ 𝑠 } ) |
15 |
7 12 14
|
3sstr4d |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ⊆ ( 𝐹 ‘ 𝑉 ) ) |