Metamath Proof Explorer

Theorem oemapso

Description: The relation T is a strict order on S (a corollary of wemapso2 ). (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 oemapso 
|- ( ph -> T Or 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 eloni 
 |-  ( B e. On -> Ord B )
6 ordwe 
 |-  ( Ord B -> _E We B )
7 weso 
 |-  ( _E We B -> _E Or B )
8 3 5 6 7 4syl 
 |-  ( ph -> _E Or B )
9 cnvso 
 |-  ( _E Or B <-> `' _E Or B )
10 8 9 sylib 
 |-  ( ph -> `' _E Or B )
11 eloni 
 |-  ( A e. On -> Ord A )
12 ordwe 
 |-  ( Ord A -> _E We A )
13 weso 
 |-  ( _E We A -> _E Or A )
14 2 11 12 13 4syl 
 |-  ( ph -> _E Or A )
15 fvex 
 |-  ( y ` z ) e. _V
16 15 epeli 
 |-  ( ( x ` z ) _E ( y ` z ) <-> ( x ` z ) e. ( y ` z ) )
17 vex 
 |-  w e. _V
18 vex 
 |-  z e. _V
19 17 18 brcnv 
 |-  ( w `' _E z <-> z _E w )
20 epel 
 |-  ( z _E w <-> z e. w )
21 19 20 bitri 
 |-  ( w `' _E z <-> z e. w )
22 21 imbi1i 
 |-  ( ( w `' _E z -> ( x ` w ) = ( y ` w ) ) <-> ( z e. w -> ( x ` w ) = ( y ` w ) ) )
23 22 ralbii 
 |-  ( A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) )
24 16 23 anbi12i 
 |-  ( ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) )
25 24 rexbii 
 |-  ( E. z e. B ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) )
26 25 opabbii 
 |-  { <. x , y >. | E. z e. B ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) } = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
27 4 26 eqtr4i 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) _E ( y ` z ) /\ A. w e. B ( w `' _E z -> ( x ` w ) = ( y ` w ) ) ) }
28 breq1 
 |-  ( g = x -> ( g finSupp (/) <-> x finSupp (/) ) )
29 28 cbvrabv 
 |-  { g e. ( A ^m B ) | g finSupp (/) } = { x e. ( A ^m B ) | x finSupp (/) }
30 27 29 wemapso2 
 |-  ( ( B e. On /\ `' _E Or B /\ _E Or A ) -> T Or { g e. ( A ^m B ) | g finSupp (/) } )
31 3 10 14 30 syl3anc 
 |-  ( ph -> T Or { g e. ( A ^m B ) | g finSupp (/) } )
32 eqid 
 |-  { g e. ( A ^m B ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) }
33 32 2 3 cantnfdm 
 |-  ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
34 1 33 eqtrid 
 |-  ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
35 soeq2 
 |-  ( S = { g e. ( A ^m B ) | g finSupp (/) } -> ( T Or S <-> T Or { g e. ( A ^m B ) | g finSupp (/) } ) )
36 34 35 syl 
 |-  ( ph -> ( T Or S <-> T Or { g e. ( A ^m B ) | g finSupp (/) } ) )
37 31 36 mpbird 
 |-  ( ph -> T Or S )