Step |
Hyp |
Ref |
Expression |
1 |
|
ineq1 |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( 𝐴 ∩ 𝐵 ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ 𝐵 ) ) |
2 |
1
|
breq1d |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) |
3 |
|
breq1 |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) 𝑀ℋ 𝐵 ) ) |
4 |
2 3
|
imbi12d |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵 ) ↔ ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ 𝐵 ) ⋖ℋ 𝐵 → if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) 𝑀ℋ 𝐵 ) ) ) |
5 |
|
ineq2 |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ 𝐵 ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ) |
6 |
|
id |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) |
7 |
5 6
|
breq12d |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ 𝐵 ) ⋖ℋ 𝐵 ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ⋖ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ) |
8 |
|
breq2 |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) 𝑀ℋ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) 𝑀ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ) |
9 |
7 8
|
imbi12d |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ 𝐵 ) ⋖ℋ 𝐵 → if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) 𝑀ℋ 𝐵 ) ↔ ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ⋖ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) 𝑀ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ) ) |
10 |
|
ifchhv |
⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∈ Cℋ |
11 |
|
ifchhv |
⊢ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ∈ Cℋ |
12 |
10 11
|
cvmdi |
⊢ ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∩ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ⋖ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) 𝑀ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) |
13 |
4 9 12
|
dedth2h |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵 ) ) |
14 |
13
|
3impia |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) → 𝐴 𝑀ℋ 𝐵 ) |