Metamath Proof Explorer

Theorem oemapvali

Description: If F < G , then there is some z witnessing this, but we can say more and in fact there is a definable expression X that also witnesses F < G . (Contributed by Mario Carneiro, 25-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 ) ) ) }
oemapval.f 
|- ( ph -> F e. S )
oemapval.g 
|- ( ph -> G e. S )
oemapvali.r 
|- ( ph -> F T G )
oemapvali.x 
|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
Assertion oemapvali 
|- ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )

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 oemapval.f 
 |-  ( ph -> F e. S )
6 oemapval.g 
 |-  ( ph -> G e. S )
7 oemapvali.r 
 |-  ( ph -> F T G )
8 oemapvali.x 
 |-  X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
9 1 2 3 4 5 6 oemapval 
 |-  ( ph -> ( F T G <-> E. z e. B ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) )
10 7 9 mpbid 
 |-  ( ph -> E. z e. B ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) )
11 ssrab2 
 |-  { c e. B | ( F ` c ) e. ( G ` c ) } C_ B
12 3 adantr 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> B e. On )
13 onss 
 |-  ( B e. On -> B C_ On )
14 12 13 syl 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> B C_ On )
15 11 14 sstrid 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } C_ On )
16 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
17 6 16 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
18 17 simprd 
 |-  ( ph -> G finSupp (/) )
19 18 adantr 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> G finSupp (/) )
20 3 3ad2ant1 
 |-  ( ( ph /\ c e. B /\ ( F ` c ) e. ( G ` c ) ) -> B e. On )
21 simp2 
 |-  ( ( ph /\ c e. B /\ ( F ` c ) e. ( G ` c ) ) -> c e. B )
22 17 simpld 
 |-  ( ph -> G : B --> A )
23 22 ffnd 
 |-  ( ph -> G Fn B )
24 23 3ad2ant1 
 |-  ( ( ph /\ c e. B /\ ( F ` c ) e. ( G ` c ) ) -> G Fn B )
25 ne0i 
 |-  ( ( F ` c ) e. ( G ` c ) -> ( G ` c ) =/= (/) )
26 25 3ad2ant3 
 |-  ( ( ph /\ c e. B /\ ( F ` c ) e. ( G ` c ) ) -> ( G ` c ) =/= (/) )
27 fvn0elsupp 
 |-  ( ( ( B e. On /\ c e. B ) /\ ( G Fn B /\ ( G ` c ) =/= (/) ) ) -> c e. ( G supp (/) ) )
28 20 21 24 26 27 syl22anc 
 |-  ( ( ph /\ c e. B /\ ( F ` c ) e. ( G ` c ) ) -> c e. ( G supp (/) ) )
29 28 rabssdv 
 |-  ( ph -> { c e. B | ( F ` c ) e. ( G ` c ) } C_ ( G supp (/) ) )
30 29 adantr 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } C_ ( G supp (/) ) )
31 fsuppimp 
 |-  ( G finSupp (/) -> ( Fun G /\ ( G supp (/) ) e. Fin ) )
32 ssfi 
 |-  ( ( ( G supp (/) ) e. Fin /\ { c e. B | ( F ` c ) e. ( G ` c ) } C_ ( G supp (/) ) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } e. Fin )
33 32 ex 
 |-  ( ( G supp (/) ) e. Fin -> ( { c e. B | ( F ` c ) e. ( G ` c ) } C_ ( G supp (/) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } e. Fin ) )
34 31 33 simpl2im 
 |-  ( G finSupp (/) -> ( { c e. B | ( F ` c ) e. ( G ` c ) } C_ ( G supp (/) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } e. Fin ) )
35 19 30 34 sylc 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } e. Fin )
36 fveq2 
 |-  ( c = z -> ( F ` c ) = ( F ` z ) )
37 fveq2 
 |-  ( c = z -> ( G ` c ) = ( G ` z ) )
38 36 37 eleq12d 
 |-  ( c = z -> ( ( F ` c ) e. ( G ` c ) <-> ( F ` z ) e. ( G ` z ) ) )
39 simprl 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> z e. B )
40 simprrl 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( F ` z ) e. ( G ` z ) )
41 38 39 40 elrabd 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> z e. { c e. B | ( F ` c ) e. ( G ` c ) } )
42 41 ne0d 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } =/= (/) )
43 ordunifi 
 |-  ( ( { c e. B | ( F ` c ) e. ( G ` c ) } C_ On /\ { c e. B | ( F ` c ) e. ( G ` c ) } e. Fin /\ { c e. B | ( F ` c ) e. ( G ` c ) } =/= (/) ) -> U. { c e. B | ( F ` c ) e. ( G ` c ) } e. { c e. B | ( F ` c ) e. ( G ` c ) } )
44 15 35 42 43 syl3anc 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> U. { c e. B | ( F ` c ) e. ( G ` c ) } e. { c e. B | ( F ` c ) e. ( G ` c ) } )
45 8 44 eqeltrid 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> X e. { c e. B | ( F ` c ) e. ( G ` c ) } )
46 11 45 sselid 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> X e. B )
47 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
48 fveq2 
 |-  ( x = X -> ( G ` x ) = ( G ` X ) )
49 47 48 eleq12d 
 |-  ( x = X -> ( ( F ` x ) e. ( G ` x ) <-> ( F ` X ) e. ( G ` X ) ) )
50 fveq2 
 |-  ( c = x -> ( F ` c ) = ( F ` x ) )
51 fveq2 
 |-  ( c = x -> ( G ` c ) = ( G ` x ) )
52 50 51 eleq12d 
 |-  ( c = x -> ( ( F ` c ) e. ( G ` c ) <-> ( F ` x ) e. ( G ` x ) ) )
53 52 cbvrabv 
 |-  { c e. B | ( F ` c ) e. ( G ` c ) } = { x e. B | ( F ` x ) e. ( G ` x ) }
54 49 53 elrab2 
 |-  ( X e. { c e. B | ( F ` c ) e. ( G ` c ) } <-> ( X e. B /\ ( F ` X ) e. ( G ` X ) ) )
55 45 54 sylib 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( X e. B /\ ( F ` X ) e. ( G ` X ) ) )
56 55 simprd 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( F ` X ) e. ( G ` X ) )
57 simprrr 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) )
58 2 adantr 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> A e. On )
59 22 adantr 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> G : B --> A )
60 59 46 ffvelcdmd 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( G ` X ) e. A )
61 onelon 
 |-  ( ( A e. On /\ ( G ` X ) e. A ) -> ( G ` X ) e. On )
62 58 60 61 syl2anc 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( G ` X ) e. On )
63 eloni 
 |-  ( ( G ` X ) e. On -> Ord ( G ` X ) )
64 ordirr 
 |-  ( Ord ( G ` X ) -> -. ( G ` X ) e. ( G ` X ) )
65 62 63 64 3syl 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> -. ( G ` X ) e. ( G ` X ) )
66 nelneq 
 |-  ( ( ( F ` X ) e. ( G ` X ) /\ -. ( G ` X ) e. ( G ` X ) ) -> -. ( F ` X ) = ( G ` X ) )
67 56 65 66 syl2anc 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> -. ( F ` X ) = ( G ` X ) )
68 eleq2 
 |-  ( w = X -> ( z e. w <-> z e. X ) )
69 fveq2 
 |-  ( w = X -> ( F ` w ) = ( F ` X ) )
70 fveq2 
 |-  ( w = X -> ( G ` w ) = ( G ` X ) )
71 69 70 eqeq12d 
 |-  ( w = X -> ( ( F ` w ) = ( G ` w ) <-> ( F ` X ) = ( G ` X ) ) )
72 68 71 imbi12d 
 |-  ( w = X -> ( ( z e. w -> ( F ` w ) = ( G ` w ) ) <-> ( z e. X -> ( F ` X ) = ( G ` X ) ) ) )
73 72 57 46 rspcdva 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( z e. X -> ( F ` X ) = ( G ` X ) ) )
74 67 73 mtod 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> -. z e. X )
75 ssexg 
 |-  ( ( { c e. B | ( F ` c ) e. ( G ` c ) } C_ B /\ B e. On ) -> { c e. B | ( F ` c ) e. ( G ` c ) } e. _V )
76 11 12 75 sylancr 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> { c e. B | ( F ` c ) e. ( G ` c ) } e. _V )
77 ssonuni 
 |-  ( { c e. B | ( F ` c ) e. ( G ` c ) } e. _V -> ( { c e. B | ( F ` c ) e. ( G ` c ) } C_ On -> U. { c e. B | ( F ` c ) e. ( G ` c ) } e. On ) )
78 76 15 77 sylc 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> U. { c e. B | ( F ` c ) e. ( G ` c ) } e. On )
79 8 78 eqeltrid 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> X e. On )
80 onelon 
 |-  ( ( B e. On /\ z e. B ) -> z e. On )
81 12 39 80 syl2anc 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> z e. On )
82 ontri1 
 |-  ( ( X e. On /\ z e. On ) -> ( X C_ z <-> -. z e. X ) )
83 79 81 82 syl2anc 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( X C_ z <-> -. z e. X ) )
84 74 83 mpbird 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> X C_ z )
85 elssuni 
 |-  ( z e. { c e. B | ( F ` c ) e. ( G ` c ) } -> z C_ U. { c e. B | ( F ` c ) e. ( G ` c ) } )
86 85 8 sseqtrrdi 
 |-  ( z e. { c e. B | ( F ` c ) e. ( G ` c ) } -> z C_ X )
87 41 86 syl 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> z C_ X )
88 84 87 eqssd 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> X = z )
89 eleq1 
 |-  ( X = z -> ( X e. w <-> z e. w ) )
90 89 imbi1d 
 |-  ( X = z -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( z e. w -> ( F ` w ) = ( G ` w ) ) ) )
91 90 ralbidv 
 |-  ( X = z -> ( A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) )
92 88 91 syl 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) )
93 57 92 mpbird 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
94 46 56 93 3jca 
 |-  ( ( ph /\ ( z e. B /\ ( ( F ` z ) e. ( G ` z ) /\ A. w e. B ( z e. w -> ( F ` w ) = ( G ` w ) ) ) ) ) -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )
95 10 94 rexlimddv 
 |-  ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )