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 )