Metamath Proof Explorer

Theorem indthincALT

Description: An alternate proof for indthinc assuming more axioms including ax-pow and ax-un . (Contributed by Zhi Wang, 17-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses indthinc.b 
|- ( ph -> B = ( Base ` C ) )
indthinc.h 
|- ( ph -> ( ( B X. B ) X. { 1o } ) = ( Hom ` C ) )
indthinc.o 
|- ( ph -> (/) = ( comp ` C ) )
indthinc.c 
|- ( ph -> C e. V )
Assertion indthincALT 
|- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) )

Proof

Step Hyp Ref Expression
1 indthinc.b 
 |-  ( ph -> B = ( Base ` C ) )
2 indthinc.h 
 |-  ( ph -> ( ( B X. B ) X. { 1o } ) = ( Hom ` C ) )
3 indthinc.o 
 |-  ( ph -> (/) = ( comp ` C ) )
4 indthinc.c 
 |-  ( ph -> C e. V )
5 1oex 
 |-  1o e. _V
6 5 ovconst2 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( ( B X. B ) X. { 1o } ) y ) = 1o )
7 domrefg 
 |-  ( 1o e. _V -> 1o ~<_ 1o )
8 5 7 ax-mp 
 |-  1o ~<_ 1o
9 6 8 eqbrtrdi 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( ( B X. B ) X. { 1o } ) y ) ~<_ 1o )
10 modom2 
 |-  ( E* f f e. ( x ( ( B X. B ) X. { 1o } ) y ) <-> ( x ( ( B X. B ) X. { 1o } ) y ) ~<_ 1o )
11 9 10 sylibr 
 |-  ( ( x e. B /\ y e. B ) -> E* f f e. ( x ( ( B X. B ) X. { 1o } ) y ) )
12 11 adantl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x ( ( B X. B ) X. { 1o } ) y ) )
13 biid 
 |-  ( ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( ( B X. B ) X. { 1o } ) y ) /\ g e. ( y ( ( B X. B ) X. { 1o } ) z ) ) ) <-> ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( ( B X. B ) X. { 1o } ) y ) /\ g e. ( y ( ( B X. B ) X. { 1o } ) z ) ) ) )
14 id 
 |-  ( y e. B -> y e. B )
15 14 ancli 
 |-  ( y e. B -> ( y e. B /\ y e. B ) )
16 5 ovconst2 
 |-  ( ( y e. B /\ y e. B ) -> ( y ( ( B X. B ) X. { 1o } ) y ) = 1o )
17 0lt1o 
 |-  (/) e. 1o
18 eleq2 
 |-  ( ( y ( ( B X. B ) X. { 1o } ) y ) = 1o -> ( (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) <-> (/) e. 1o ) )
19 17 18 mpbiri 
 |-  ( ( y ( ( B X. B ) X. { 1o } ) y ) = 1o -> (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) )
20 15 16 19 3syl 
 |-  ( y e. B -> (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) )
21 20 adantl 
 |-  ( ( ph /\ y e. B ) -> (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) )
22 17 a1i 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> (/) e. 1o )
23 0ov 
 |-  ( <. x , y >. (/) z ) = (/)
24 23 oveqi 
 |-  ( g ( <. x , y >. (/) z ) f ) = ( g (/) f )
25 0ov 
 |-  ( g (/) f ) = (/)
26 24 25 eqtri 
 |-  ( g ( <. x , y >. (/) z ) f ) = (/)
27 26 a1i 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> ( g ( <. x , y >. (/) z ) f ) = (/) )
28 5 ovconst2 
 |-  ( ( x e. B /\ z e. B ) -> ( x ( ( B X. B ) X. { 1o } ) z ) = 1o )
29 28 3adant2 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> ( x ( ( B X. B ) X. { 1o } ) z ) = 1o )
30 22 27 29 3eltr4d 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> ( g ( <. x , y >. (/) z ) f ) e. ( x ( ( B X. B ) X. { 1o } ) z ) )
31 30 ad2antrl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( ( B X. B ) X. { 1o } ) y ) /\ g e. ( y ( ( B X. B ) X. { 1o } ) z ) ) ) ) -> ( g ( <. x , y >. (/) z ) f ) e. ( x ( ( B X. B ) X. { 1o } ) z ) )
32 1 2 12 3 4 13 21 31 isthincd2 
 |-  ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) )