This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincmoALT

Description: Alternate proof of thincmo . (Contributed by Zhi Wang, 21-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses thincmo.c ⊢ φ → C ∈ ThinCat
thincmo.x ⊢ φ → X ∈ B
thincmo.y ⊢ φ → Y ∈ B
thincmo.b ⊢ B = Base C
thincmo.h ⊢ H = Hom ⁡ C
Assertion thincmoALT ⊢ φ → ∃* f f ∈ X H Y

Proof

Step Hyp Ref Expression
1 thincmo.c ⊢ φ → C ∈ ThinCat
2 thincmo.x ⊢ φ → X ∈ B
3 thincmo.y ⊢ φ → Y ∈ B
4 thincmo.b ⊢ B = Base C
5 thincmo.h ⊢ H = Hom ⁡ C
6 4 5 isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
7 6 simprbi ⊢ C ∈ ThinCat → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
8 1 7 syl ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
9 oveq12 ⊢ x = X ∧ y = Y → x H y = X H Y
10 9 eleq2d ⊢ x = X ∧ y = Y → f ∈ x H y ↔ f ∈ X H Y
11 10 mobidv ⊢ x = X ∧ y = Y → ∃* f f ∈ x H y ↔ ∃* f f ∈ X H Y
12 11 rspc2gv ⊢ X ∈ B ∧ Y ∈ B → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y → ∃* f f ∈ X H Y
13 2 3 12 syl2anc ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y → ∃* f f ∈ X H Y
14 8 13 mpd ⊢ φ → ∃* f f ∈ X H Y