Step |
Hyp |
Ref |
Expression |
1 |
|
sseq1 |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ⊆ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ 𝐵 ) ) |
2 |
|
breq1 |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 𝐶ℋ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) ) |
3 |
1 2
|
imbi12d |
⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 ⊆ 𝐵 → 𝐴 𝐶ℋ 𝐵 ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ 𝐵 → if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) ) ) |
4 |
|
sseq2 |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) ) |
5 |
|
breq2 |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) ) |
6 |
4 5
|
imbi12d |
⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ 𝐵 → if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ 𝐵 ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) ) ) |
7 |
|
h0elch |
⊢ 0ℋ ∈ Cℋ |
8 |
7
|
elimel |
⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ |
9 |
7
|
elimel |
⊢ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ∈ Cℋ |
10 |
8 9
|
lecmi |
⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⊆ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) → if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) 𝐶ℋ if ( 𝐵 ∈ Cℋ , 𝐵 , 0ℋ ) ) |
11 |
3 6 10
|
dedth2h |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 → 𝐴 𝐶ℋ 𝐵 ) ) |
12 |
11
|
3impia |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 𝐶ℋ 𝐵 ) |