Step |
Hyp |
Ref |
Expression |
1 |
|
inidm |
⊢ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ( 𝐼 ‘ ∅ ) |
2 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝐵 |
3 |
|
ineq1 |
⊢ ( 𝑠 = ∅ → ( 𝑠 ∩ 𝑡 ) = ( ∅ ∩ 𝑡 ) ) |
4 |
3
|
eqeq1d |
⊢ ( 𝑠 = ∅ → ( ( 𝑠 ∩ 𝑡 ) = ∅ ↔ ( ∅ ∩ 𝑡 ) = ∅ ) ) |
5 |
|
fveq2 |
⊢ ( 𝑠 = ∅ → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ ∅ ) ) |
6 |
5
|
ineq1d |
⊢ ( 𝑠 = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) |
7 |
6
|
eqeq1d |
⊢ ( 𝑠 = ∅ → ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) |
8 |
4 7
|
imbi12d |
⊢ ( 𝑠 = ∅ → ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) ) |
9 |
|
0in |
⊢ ( ∅ ∩ 𝑡 ) = ∅ |
10 |
|
pm5.5 |
⊢ ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) |
11 |
9 10
|
ax-mp |
⊢ ( ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) |
12 |
8 11
|
syl6bb |
⊢ ( 𝑠 = ∅ → ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) |
13 |
|
fveq2 |
⊢ ( 𝑡 = ∅ → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ ∅ ) ) |
14 |
13
|
ineq2d |
⊢ ( 𝑡 = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) ) |
15 |
14
|
eqeq1d |
⊢ ( 𝑡 = ∅ → ( ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) ) |
16 |
12 15
|
rspc2v |
⊢ ( ( ∅ ∈ 𝒫 𝐵 ∧ ∅ ∈ 𝒫 𝐵 ) → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) ) |
17 |
2 2 16
|
mp2an |
⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) |
18 |
1 17
|
syl5eqr |
⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) → ( 𝐼 ‘ ∅ ) = ∅ ) |