Step |
Hyp |
Ref |
Expression |
1 |
|
inteq |
⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ∩ 𝐴 = ∩ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ) |
2 |
1
|
eleq1d |
⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( ∩ 𝐴 ∈ Sℋ ↔ ∩ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ∈ Sℋ ) ) |
3 |
|
sseq1 |
⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( 𝐴 ⊆ Sℋ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ) ) |
4 |
|
neeq1 |
⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( 𝐴 ≠ ∅ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) ) |
5 |
3 4
|
anbi12d |
⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) ↔ ( if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ∧ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) ) ) |
6 |
|
sseq1 |
⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( Sℋ ⊆ Sℋ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ) ) |
7 |
|
neeq1 |
⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( Sℋ ≠ ∅ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) ) |
8 |
6 7
|
anbi12d |
⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( ( Sℋ ⊆ Sℋ ∧ Sℋ ≠ ∅ ) ↔ ( if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ∧ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) ) ) |
9 |
|
ssid |
⊢ Sℋ ⊆ Sℋ |
10 |
|
h0elsh |
⊢ 0ℋ ∈ Sℋ |
11 |
10
|
ne0ii |
⊢ Sℋ ≠ ∅ |
12 |
9 11
|
pm3.2i |
⊢ ( Sℋ ⊆ Sℋ ∧ Sℋ ≠ ∅ ) |
13 |
5 8 12
|
elimhyp |
⊢ ( if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ∧ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) |
14 |
13
|
shintcli |
⊢ ∩ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ∈ Sℋ |
15 |
2 14
|
dedth |
⊢ ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Sℋ ) |