Metamath Proof Explorer

Theorem thincmoALT

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

Ref Expression
Hypotheses thincmo.c No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
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 Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
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 Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) with typecode |-
7 6 simprbi Could not format ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) ) : No typesetting found for |- ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) ) with typecode |-
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