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

Metamath Proof Explorer

Theorem isuplem

Description: Lemma for isup and other theorems. (Contributed by Zhi Wang, 25-Sep-2025)

Ref Expression
Hypotheses upfval.b ⊢ B = Base D
upfval.c ⊢ C = Base E
upfval.h ⊢ H = Hom ⁡ D
upfval.j ⊢ J = Hom ⁡ E
upfval.o ⊢ O = comp ⁡ E
upfval2.w ⊢ φ → W ∈ C
upfval3.f ⊢ φ → F D Func E G
Assertion isuplem Could not format assertion : No typesetting found for |- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 upfval.b ⊢ B = Base D
2 upfval.c ⊢ C = Base E
3 upfval.h ⊢ H = Hom ⁡ D
4 upfval.j ⊢ J = Hom ⁡ E
5 upfval.o ⊢ O = comp ⁡ E
6 upfval2.w ⊢ φ → W ∈ C
7 upfval3.f ⊢ φ → F D Func E G
8 1 2 3 4 5 6 7 upfval3 Could not format ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } ) : No typesetting found for |- ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. | ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } ) with typecode |-
9 oveq1 ⊢ x = X → x H y = X H y
10 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
11 10 opeq2d ⊢ x = X → W F ⁡ x = W F ⁡ X
12 11 oveq1d ⊢ x = X → W F ⁡ x O F ⁡ y = W F ⁡ X O F ⁡ y
13 oveq1 ⊢ x = X → x G y = X G y
14 13 fveq1d ⊢ x = X → x G y ⁡ k = X G y ⁡ k
15 eqidd ⊢ x = X → m = m
16 12 14 15 oveq123d ⊢ x = X → x G y ⁡ k W F ⁡ x O F ⁡ y m = X G y ⁡ k W F ⁡ X O F ⁡ y m
17 16 eqeq2d ⊢ x = X → g = x G y ⁡ k W F ⁡ x O F ⁡ y m ↔ g = X G y ⁡ k W F ⁡ X O F ⁡ y m
18 9 17 reueqbidv ⊢ x = X → ∃! k ∈ x H y g = x G y ⁡ k W F ⁡ x O F ⁡ y m ↔ ∃! k ∈ X H y g = X G y ⁡ k W F ⁡ X O F ⁡ y m
19 18 2ralbidv ⊢ x = X → ∀ y ∈ B ∀ g ∈ W J F ⁡ y ∃! k ∈ x H y g = x G y ⁡ k W F ⁡ x O F ⁡ y m ↔ ∀ y ∈ B ∀ g ∈ W J F ⁡ y ∃! k ∈ X H y g = X G y ⁡ k W F ⁡ X O F ⁡ y m
20 oveq2 ⊢ m = M → X G y ⁡ k W F ⁡ X O F ⁡ y m = X G y ⁡ k W F ⁡ X O F ⁡ y M
21 20 eqeq2d ⊢ m = M → g = X G y ⁡ k W F ⁡ X O F ⁡ y m ↔ g = X G y ⁡ k W F ⁡ X O F ⁡ y M
22 21 reubidv ⊢ m = M → ∃! k ∈ X H y g = X G y ⁡ k W F ⁡ X O F ⁡ y m ↔ ∃! k ∈ X H y g = X G y ⁡ k W F ⁡ X O F ⁡ y M
23 22 2ralbidv ⊢ m = M → ∀ y ∈ B ∀ g ∈ W J F ⁡ y ∃! k ∈ X H y g = X G y ⁡ k W F ⁡ X O F ⁡ y m ↔ ∀ y ∈ B ∀ g ∈ W J F ⁡ y ∃! k ∈ X H y g = X G y ⁡ k W F ⁡ X O F ⁡ y M
24 eqidd ⊢ x = X ∧ m = M → B = B
25 simpl ⊢ x = X ∧ m = M → x = X
26 25 fveq2d ⊢ x = X ∧ m = M → F ⁡ x = F ⁡ X
27 26 oveq2d ⊢ x = X ∧ m = M → W J F ⁡ x = W J F ⁡ X
28 8 19 23 24 27 brab2ddw Could not format ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) : No typesetting found for |- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) with typecode |-