Metamath Proof Explorer

Theorem omxpenlem

Description: Lemma for omxpen . (Contributed by Mario Carneiro, 3-Mar-2013) (Revised by Mario Carneiro, 25-May-2015)

Ref Expression
Hypothesis omxpenlem.1 
|- F = ( x e. B , y e. A |-> ( ( A .o x ) +o y ) )
Assertion omxpenlem 
|- ( ( A e. On /\ B e. On ) -> F : ( B X. A ) -1-1-onto-> ( A .o B ) )

Proof

Step Hyp Ref Expression
1 omxpenlem.1 
 |-  F = ( x e. B , y e. A |-> ( ( A .o x ) +o y ) )
2 eloni 
 |-  ( B e. On -> Ord B )
3 2 ad2antlr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> Ord B )
4 simprl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> x e. B )
5 ordsucss 
 |-  ( Ord B -> ( x e. B -> suc x C_ B ) )
6 3 4 5 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> suc x C_ B )
7 onelon 
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
8 7 ad2ant2lr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> x e. On )
9 onsuc 
 |-  ( x e. On -> suc x e. On )
10 8 9 syl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> suc x e. On )
11 simplr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> B e. On )
12 simpll 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> A e. On )
13 omwordi 
 |-  ( ( suc x e. On /\ B e. On /\ A e. On ) -> ( suc x C_ B -> ( A .o suc x ) C_ ( A .o B ) ) )
14 10 11 12 13 syl3anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( suc x C_ B -> ( A .o suc x ) C_ ( A .o B ) ) )
15 6 14 mpd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( A .o suc x ) C_ ( A .o B ) )
16 simprr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> y e. A )
17 onelon 
 |-  ( ( A e. On /\ y e. A ) -> y e. On )
18 17 ad2ant2rl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> y e. On )
19 omcl 
 |-  ( ( A e. On /\ x e. On ) -> ( A .o x ) e. On )
20 12 8 19 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( A .o x ) e. On )
21 oaord 
 |-  ( ( y e. On /\ A e. On /\ ( A .o x ) e. On ) -> ( y e. A <-> ( ( A .o x ) +o y ) e. ( ( A .o x ) +o A ) ) )
22 18 12 20 21 syl3anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( y e. A <-> ( ( A .o x ) +o y ) e. ( ( A .o x ) +o A ) ) )
23 16 22 mpbid 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( ( A .o x ) +o y ) e. ( ( A .o x ) +o A ) )
24 omsuc 
 |-  ( ( A e. On /\ x e. On ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
25 12 8 24 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
26 23 25 eleqtrrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( ( A .o x ) +o y ) e. ( A .o suc x ) )
27 15 26 sseldd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. B /\ y e. A ) ) -> ( ( A .o x ) +o y ) e. ( A .o B ) )
28 27 ralrimivva 
 |-  ( ( A e. On /\ B e. On ) -> A. x e. B A. y e. A ( ( A .o x ) +o y ) e. ( A .o B ) )
29 1 fmpo 
 |-  ( A. x e. B A. y e. A ( ( A .o x ) +o y ) e. ( A .o B ) <-> F : ( B X. A ) --> ( A .o B ) )
30 28 29 sylib 
 |-  ( ( A e. On /\ B e. On ) -> F : ( B X. A ) --> ( A .o B ) )
31 30 ffnd 
 |-  ( ( A e. On /\ B e. On ) -> F Fn ( B X. A ) )
32 simpll 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> A e. On )
33 omcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
34 onelon 
 |-  ( ( ( A .o B ) e. On /\ m e. ( A .o B ) ) -> m e. On )
35 33 34 sylan 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> m e. On )
36 noel 
 |-  -. m e. (/)
37 oveq1 
 |-  ( A = (/) -> ( A .o B ) = ( (/) .o B ) )
38 om0r 
 |-  ( B e. On -> ( (/) .o B ) = (/) )
39 37 38 sylan9eqr 
 |-  ( ( B e. On /\ A = (/) ) -> ( A .o B ) = (/) )
40 39 eleq2d 
 |-  ( ( B e. On /\ A = (/) ) -> ( m e. ( A .o B ) <-> m e. (/) ) )
41 36 40 mtbiri 
 |-  ( ( B e. On /\ A = (/) ) -> -. m e. ( A .o B ) )
42 41 ex 
 |-  ( B e. On -> ( A = (/) -> -. m e. ( A .o B ) ) )
43 42 necon2ad 
 |-  ( B e. On -> ( m e. ( A .o B ) -> A =/= (/) ) )
44 43 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( m e. ( A .o B ) -> A =/= (/) ) )
45 44 imp 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> A =/= (/) )
46 omeu 
 |-  ( ( A e. On /\ m e. On /\ A =/= (/) ) -> E! n E. x e. On E. y e. A ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) )
47 32 35 45 46 syl3anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> E! n E. x e. On E. y e. A ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) )
48 vex 
 |-  m e. _V
49 vex 
 |-  n e. _V
50 48 49 brcnv 
 |-  ( m `' F n <-> n F m )
51 eleq1 
 |-  ( m = ( ( A .o x ) +o y ) -> ( m e. ( A .o B ) <-> ( ( A .o x ) +o y ) e. ( A .o B ) ) )
52 51 biimpac 
 |-  ( ( m e. ( A .o B ) /\ m = ( ( A .o x ) +o y ) ) -> ( ( A .o x ) +o y ) e. ( A .o B ) )
53 7 ex 
 |-  ( B e. On -> ( x e. B -> x e. On ) )
54 53 ad2antlr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) -> ( x e. B -> x e. On ) )
55 simplll 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> A e. On )
56 simpr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> x e. On )
57 55 56 19 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( A .o x ) e. On )
58 simplrr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> y e. A )
59 55 58 17 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> y e. On )
60 oaword1 
 |-  ( ( ( A .o x ) e. On /\ y e. On ) -> ( A .o x ) C_ ( ( A .o x ) +o y ) )
61 57 59 60 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( A .o x ) C_ ( ( A .o x ) +o y ) )
62 simplrl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( ( A .o x ) +o y ) e. ( A .o B ) )
63 33 ad2antrr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( A .o B ) e. On )
64 ontr2 
 |-  ( ( ( A .o x ) e. On /\ ( A .o B ) e. On ) -> ( ( ( A .o x ) C_ ( ( A .o x ) +o y ) /\ ( ( A .o x ) +o y ) e. ( A .o B ) ) -> ( A .o x ) e. ( A .o B ) ) )
65 57 63 64 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( ( ( A .o x ) C_ ( ( A .o x ) +o y ) /\ ( ( A .o x ) +o y ) e. ( A .o B ) ) -> ( A .o x ) e. ( A .o B ) ) )
66 61 62 65 mp2and 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( A .o x ) e. ( A .o B ) )
67 simpllr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> B e. On )
68 62 ne0d 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( A .o B ) =/= (/) )
69 on0eln0 
 |-  ( ( A .o B ) e. On -> ( (/) e. ( A .o B ) <-> ( A .o B ) =/= (/) ) )
70 63 69 syl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( (/) e. ( A .o B ) <-> ( A .o B ) =/= (/) ) )
71 68 70 mpbird 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> (/) e. ( A .o B ) )
72 om00el 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. ( A .o B ) <-> ( (/) e. A /\ (/) e. B ) ) )
73 72 ad2antrr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( (/) e. ( A .o B ) <-> ( (/) e. A /\ (/) e. B ) ) )
74 71 73 mpbid 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( (/) e. A /\ (/) e. B ) )
75 74 simpld 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> (/) e. A )
76 omord2 
 |-  ( ( ( x e. On /\ B e. On /\ A e. On ) /\ (/) e. A ) -> ( x e. B <-> ( A .o x ) e. ( A .o B ) ) )
77 56 67 55 75 76 syl31anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> ( x e. B <-> ( A .o x ) e. ( A .o B ) ) )
78 66 77 mpbird 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) /\ x e. On ) -> x e. B )
79 78 ex 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) -> ( x e. On -> x e. B ) )
80 54 79 impbid 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( ( ( A .o x ) +o y ) e. ( A .o B ) /\ y e. A ) ) -> ( x e. B <-> x e. On ) )
81 80 expr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( ( A .o x ) +o y ) e. ( A .o B ) ) -> ( y e. A -> ( x e. B <-> x e. On ) ) )
82 81 pm5.32rd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( ( A .o x ) +o y ) e. ( A .o B ) ) -> ( ( x e. B /\ y e. A ) <-> ( x e. On /\ y e. A ) ) )
83 52 82 sylan2 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( m e. ( A .o B ) /\ m = ( ( A .o x ) +o y ) ) ) -> ( ( x e. B /\ y e. A ) <-> ( x e. On /\ y e. A ) ) )
84 83 expr 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( m = ( ( A .o x ) +o y ) -> ( ( x e. B /\ y e. A ) <-> ( x e. On /\ y e. A ) ) ) )
85 84 pm5.32rd 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) <-> ( ( x e. On /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) )
86 eqcom 
 |-  ( m = ( ( A .o x ) +o y ) <-> ( ( A .o x ) +o y ) = m )
87 86 anbi2i 
 |-  ( ( ( x e. On /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) <-> ( ( x e. On /\ y e. A ) /\ ( ( A .o x ) +o y ) = m ) )
88 85 87 bitrdi 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) <-> ( ( x e. On /\ y e. A ) /\ ( ( A .o x ) +o y ) = m ) ) )
89 88 anbi2d 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) <-> ( n = <. x , y >. /\ ( ( x e. On /\ y e. A ) /\ ( ( A .o x ) +o y ) = m ) ) ) )
90 an12 
 |-  ( ( n = <. x , y >. /\ ( ( x e. On /\ y e. A ) /\ ( ( A .o x ) +o y ) = m ) ) <-> ( ( x e. On /\ y e. A ) /\ ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) ) )
91 89 90 bitrdi 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) <-> ( ( x e. On /\ y e. A ) /\ ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) ) ) )
92 91 2exbidv 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) <-> E. x E. y ( ( x e. On /\ y e. A ) /\ ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) ) ) )
93 df-mpo 
 |-  ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) = { <. <. x , y >. , m >. | ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) }
94 dfoprab2 
 |-  { <. <. x , y >. , m >. | ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) } = { <. n , m >. | E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) }
95 1 93 94 3eqtri 
 |-  F = { <. n , m >. | E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) }
96 95 breqi 
 |-  ( n F m <-> n { <. n , m >. | E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) } m )
97 df-br 
 |-  ( n { <. n , m >. | E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) } m <-> <. n , m >. e. { <. n , m >. | E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) } )
98 opabidw 
 |-  ( <. n , m >. e. { <. n , m >. | E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) } <-> E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) )
99 96 97 98 3bitri 
 |-  ( n F m <-> E. x E. y ( n = <. x , y >. /\ ( ( x e. B /\ y e. A ) /\ m = ( ( A .o x ) +o y ) ) ) )
100 r2ex 
 |-  ( E. x e. On E. y e. A ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) <-> E. x E. y ( ( x e. On /\ y e. A ) /\ ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) ) )
101 92 99 100 3bitr4g 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( n F m <-> E. x e. On E. y e. A ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) ) )
102 50 101 bitrid 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( m `' F n <-> E. x e. On E. y e. A ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) ) )
103 102 eubidv 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> ( E! n m `' F n <-> E! n E. x e. On E. y e. A ( n = <. x , y >. /\ ( ( A .o x ) +o y ) = m ) ) )
104 47 103 mpbird 
 |-  ( ( ( A e. On /\ B e. On ) /\ m e. ( A .o B ) ) -> E! n m `' F n )
105 104 ralrimiva 
 |-  ( ( A e. On /\ B e. On ) -> A. m e. ( A .o B ) E! n m `' F n )
106 fnres 
 |-  ( ( `' F |` ( A .o B ) ) Fn ( A .o B ) <-> A. m e. ( A .o B ) E! n m `' F n )
107 105 106 sylibr 
 |-  ( ( A e. On /\ B e. On ) -> ( `' F |` ( A .o B ) ) Fn ( A .o B ) )
108 relcnv 
 |-  Rel `' F
109 df-rn 
 |-  ran F = dom `' F
110 30 frnd 
 |-  ( ( A e. On /\ B e. On ) -> ran F C_ ( A .o B ) )
111 109 110 eqsstrrid 
 |-  ( ( A e. On /\ B e. On ) -> dom `' F C_ ( A .o B ) )
112 relssres 
 |-  ( ( Rel `' F /\ dom `' F C_ ( A .o B ) ) -> ( `' F |` ( A .o B ) ) = `' F )
113 108 111 112 sylancr 
 |-  ( ( A e. On /\ B e. On ) -> ( `' F |` ( A .o B ) ) = `' F )
114 113 fneq1d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( `' F |` ( A .o B ) ) Fn ( A .o B ) <-> `' F Fn ( A .o B ) ) )
115 107 114 mpbid 
 |-  ( ( A e. On /\ B e. On ) -> `' F Fn ( A .o B ) )
116 dff1o4 
 |-  ( F : ( B X. A ) -1-1-onto-> ( A .o B ) <-> ( F Fn ( B X. A ) /\ `' F Fn ( A .o B ) ) )
117 31 115 116 sylanbrc 
 |-  ( ( A e. On /\ B e. On ) -> F : ( B X. A ) -1-1-onto-> ( A .o B ) )