Step |
Hyp |
Ref |
Expression |
1 |
|
isinito.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
2 |
|
isinito.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
3 |
|
isinito.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
4 |
|
isinito.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝐵 ) |
5 |
3 1 2
|
termoval |
⊢ ( 𝜑 → ( TermO ‘ 𝐶 ) = { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝑖 ) } ) |
6 |
5
|
eleq2d |
⊢ ( 𝜑 → ( 𝐼 ∈ ( TermO ‘ 𝐶 ) ↔ 𝐼 ∈ { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝑖 ) } ) ) |
7 |
|
oveq2 |
⊢ ( 𝑖 = 𝐼 → ( 𝑏 𝐻 𝑖 ) = ( 𝑏 𝐻 𝐼 ) ) |
8 |
7
|
eleq2d |
⊢ ( 𝑖 = 𝐼 → ( ℎ ∈ ( 𝑏 𝐻 𝑖 ) ↔ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) ) |
9 |
8
|
eubidv |
⊢ ( 𝑖 = 𝐼 → ( ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝑖 ) ↔ ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) ) |
10 |
9
|
ralbidv |
⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝑖 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) ) |
11 |
10
|
elrab3 |
⊢ ( 𝐼 ∈ 𝐵 → ( 𝐼 ∈ { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝑖 ) } ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) ) |
12 |
4 11
|
syl |
⊢ ( 𝜑 → ( 𝐼 ∈ { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝑖 ) } ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) ) |
13 |
6 12
|
bitrd |
⊢ ( 𝜑 → ( 𝐼 ∈ ( TermO ‘ 𝐶 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) ) |