Metamath Proof Explorer

Theorem cantnffval2

Description: An alternate definition of df-cnf which relies on cantnf . (Note that although the use of S seems self-referential, one can use cantnfdm to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
oemapval.t 
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
Assertion cantnffval2 
|- ( ph -> ( A CNF B ) = `' OrdIso ( T , S ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 oemapval.t 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 1 2 3 4 cantnf 
 |-  ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) )
6 isof1o 
 |-  ( ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) -> ( A CNF B ) : S -1-1-onto-> ( A ^o B ) )
7 f1orel 
 |-  ( ( A CNF B ) : S -1-1-onto-> ( A ^o B ) -> Rel ( A CNF B ) )
8 5 6 7 3syl 
 |-  ( ph -> Rel ( A CNF B ) )
9 dfrel2 
 |-  ( Rel ( A CNF B ) <-> `' `' ( A CNF B ) = ( A CNF B ) )
10 8 9 sylib 
 |-  ( ph -> `' `' ( A CNF B ) = ( A CNF B ) )
11 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
12 2 3 11 syl2anc 
 |-  ( ph -> ( A ^o B ) e. On )
13 eloni 
 |-  ( ( A ^o B ) e. On -> Ord ( A ^o B ) )
14 12 13 syl 
 |-  ( ph -> Ord ( A ^o B ) )
15 isocnv 
 |-  ( ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) -> `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) )
16 5 15 syl 
 |-  ( ph -> `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) )
17 1 2 3 4 oemapwe 
 |-  ( ph -> ( T We S /\ dom OrdIso ( T , S ) = ( A ^o B ) ) )
18 17 simpld 
 |-  ( ph -> T We S )
19 ovex 
 |-  ( A CNF B ) e. _V
20 19 dmex 
 |-  dom ( A CNF B ) e. _V
21 1 20 eqeltri 
 |-  S e. _V
22 exse 
 |-  ( S e. _V -> T Se S )
23 21 22 ax-mp 
 |-  T Se S
24 eqid 
 |-  OrdIso ( T , S ) = OrdIso ( T , S )
25 24 oieu 
 |-  ( ( T We S /\ T Se S ) -> ( ( Ord ( A ^o B ) /\ `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) <-> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) ) )
26 18 23 25 sylancl 
 |-  ( ph -> ( ( Ord ( A ^o B ) /\ `' ( A CNF B ) Isom _E , T ( ( A ^o B ) , S ) ) <-> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) ) )
27 14 16 26 mpbi2and 
 |-  ( ph -> ( ( A ^o B ) = dom OrdIso ( T , S ) /\ `' ( A CNF B ) = OrdIso ( T , S ) ) )
28 27 simprd 
 |-  ( ph -> `' ( A CNF B ) = OrdIso ( T , S ) )
29 28 cnveqd 
 |-  ( ph -> `' `' ( A CNF B ) = `' OrdIso ( T , S ) )
30 10 29 eqtr3d 
 |-  ( ph -> ( A CNF B ) = `' OrdIso ( T , S ) )