Step |
Hyp |
Ref |
Expression |
1 |
|
cnvbraval |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) |
2 |
|
cnvbracl |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) ∈ ℋ ) |
3 |
1 2
|
eqeltrrd |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ∈ ℋ ) |
4 |
|
bra11 |
⊢ bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) |
5 |
|
f1ocnvfvb |
⊢ ( ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ∧ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ∈ ℋ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ( bra ‘ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 ↔ ( ◡ bra ‘ 𝑇 ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) ) |
6 |
4 5
|
mp3an1 |
⊢ ( ( ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ∈ ℋ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ( bra ‘ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 ↔ ( ◡ bra ‘ 𝑇 ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) ) |
7 |
3 6
|
mpancom |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ( bra ‘ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 ↔ ( ◡ bra ‘ 𝑇 ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) ) |
8 |
1 7
|
mpbird |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( bra ‘ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 ) |
9 |
8
|
eqcomd |
⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → 𝑇 = ( bra ‘ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) ) |