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

Metamath Proof Explorer

Theorem postcposALT

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

Ref Expression
Hypotheses postc.c 
|- ( ph -> C = ( ProsetToCat ` K ) )
postc.k 
|- ( ph -> K e. Proset )
Assertion postcposALT 
|- ( ph -> ( K e. Poset <-> C e. Poset ) )

Proof

Step Hyp Ref Expression
1 postc.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 postc.k 
 |-  ( ph -> K e. Proset )
3 eqidd 
 |-  ( ph -> ( Base ` K ) = ( Base ` K ) )
4 1 2 3 prstcbas 
 |-  ( ph -> ( Base ` K ) = ( Base ` C ) )
5 eqidd 
 |-  ( ph -> ( le ` K ) = ( le ` K ) )
6 1 2 5 prstcle 
 |-  ( ph -> ( x ( le ` K ) y <-> x ( le ` C ) y ) )
7 1 2 5 prstcle 
 |-  ( ph -> ( y ( le ` K ) x <-> y ( le ` C ) x ) )
8 6 7 anbi12d 
 |-  ( ph -> ( ( x ( le ` K ) y /\ y ( le ` K ) x ) <-> ( x ( le ` C ) y /\ y ( le ` C ) x ) ) )
9 8 imbi1d 
 |-  ( ph -> ( ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) <-> ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
10 4 9 raleqbidvv 
 |-  ( ph -> ( A. y e. ( Base ` K ) ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) <-> A. y e. ( Base ` C ) ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
11 4 10 raleqbidvv 
 |-  ( ph -> ( A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
12 eqid 
 |-  ( Base ` K ) = ( Base ` K )
13 eqid 
 |-  ( le ` K ) = ( le ` K )
14 12 13 ispos2 
 |-  ( K e. Poset <-> ( K e. Proset /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) ) )
15 14 baib 
 |-  ( K e. Proset -> ( K e. Poset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) ) )
16 2 15 syl 
 |-  ( ph -> ( K e. Poset <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) ) )
17 1 2 prstcprs 
 |-  ( ph -> C e. Proset )
18 eqid 
 |-  ( Base ` C ) = ( Base ` C )
19 eqid 
 |-  ( le ` C ) = ( le ` C )
20 18 19 ispos2 
 |-  ( C e. Poset <-> ( C e. Proset /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
21 20 baib 
 |-  ( C e. Proset -> ( C e. Poset <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
22 17 21 syl 
 |-  ( ph -> ( C e. Poset <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( ( x ( le ` C ) y /\ y ( le ` C ) x ) -> x = y ) ) )
23 11 16 22 3bitr4d 
 |-  ( ph -> ( K e. Poset <-> C e. Poset ) )