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=xB,yAA𝑜x+𝑜y
Assertion omxpenlem AOnBOnF:B×A1-1 ontoA𝑜B

Proof

Step Hyp Ref Expression
1 omxpenlem.1 F=xB,yAA𝑜x+𝑜y
2 eloni BOnOrdB
3 2 ad2antlr AOnBOnxByAOrdB
4 simprl AOnBOnxByAxB
5 ordsucss OrdBxBsucxB
6 3 4 5 sylc AOnBOnxByAsucxB
7 onelon BOnxBxOn
8 7 ad2ant2lr AOnBOnxByAxOn
9 suceloni xOnsucxOn
10 8 9 syl AOnBOnxByAsucxOn
11 simplr AOnBOnxByABOn
12 simpll AOnBOnxByAAOn
13 omwordi sucxOnBOnAOnsucxBA𝑜sucxA𝑜B
14 10 11 12 13 syl3anc AOnBOnxByAsucxBA𝑜sucxA𝑜B
15 6 14 mpd AOnBOnxByAA𝑜sucxA𝑜B
16 simprr AOnBOnxByAyA
17 onelon AOnyAyOn
18 17 ad2ant2rl AOnBOnxByAyOn
19 omcl AOnxOnA𝑜xOn
20 12 8 19 syl2anc AOnBOnxByAA𝑜xOn
21 oaord yOnAOnA𝑜xOnyAA𝑜x+𝑜yA𝑜x+𝑜A
22 18 12 20 21 syl3anc AOnBOnxByAyAA𝑜x+𝑜yA𝑜x+𝑜A
23 16 22 mpbid AOnBOnxByAA𝑜x+𝑜yA𝑜x+𝑜A
24 omsuc AOnxOnA𝑜sucx=A𝑜x+𝑜A
25 12 8 24 syl2anc AOnBOnxByAA𝑜sucx=A𝑜x+𝑜A
26 23 25 eleqtrrd AOnBOnxByAA𝑜x+𝑜yA𝑜sucx
27 15 26 sseldd AOnBOnxByAA𝑜x+𝑜yA𝑜B
28 27 ralrimivva AOnBOnxByAA𝑜x+𝑜yA𝑜B
29 1 fmpo xByAA𝑜x+𝑜yA𝑜BF:B×AA𝑜B
30 28 29 sylib AOnBOnF:B×AA𝑜B
31 30 ffnd AOnBOnFFnB×A
32 simpll AOnBOnmA𝑜BAOn
33 omcl AOnBOnA𝑜BOn
34 onelon A𝑜BOnmA𝑜BmOn
35 33 34 sylan AOnBOnmA𝑜BmOn
36 noel ¬m
37 oveq1 A=A𝑜B=𝑜B
38 om0r BOn𝑜B=
39 37 38 sylan9eqr BOnA=A𝑜B=
40 39 eleq2d BOnA=mA𝑜Bm
41 36 40 mtbiri BOnA=¬mA𝑜B
42 41 ex BOnA=¬mA𝑜B
43 42 necon2ad BOnmA𝑜BA
44 43 adantl AOnBOnmA𝑜BA
45 44 imp AOnBOnmA𝑜BA
46 omeu AOnmOnA∃!nxOnyAn=xyA𝑜x+𝑜y=m
47 32 35 45 46 syl3anc AOnBOnmA𝑜B∃!nxOnyAn=xyA𝑜x+𝑜y=m
48 vex mV
49 vex nV
50 48 49 brcnv mF-1nnFm
51 eleq1 m=A𝑜x+𝑜ymA𝑜BA𝑜x+𝑜yA𝑜B
52 51 biimpac mA𝑜Bm=A𝑜x+𝑜yA𝑜x+𝑜yA𝑜B
53 7 ex BOnxBxOn
54 53 ad2antlr AOnBOnA𝑜x+𝑜yA𝑜ByAxBxOn
55 simplll AOnBOnA𝑜x+𝑜yA𝑜ByAxOnAOn
56 simpr AOnBOnA𝑜x+𝑜yA𝑜ByAxOnxOn
57 55 56 19 syl2anc AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜xOn
58 simplrr AOnBOnA𝑜x+𝑜yA𝑜ByAxOnyA
59 55 58 17 syl2anc AOnBOnA𝑜x+𝑜yA𝑜ByAxOnyOn
60 oaword1 A𝑜xOnyOnA𝑜xA𝑜x+𝑜y
61 57 59 60 syl2anc AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜xA𝑜x+𝑜y
62 simplrl AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜x+𝑜yA𝑜B
63 33 ad2antrr AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜BOn
64 ontr2 A𝑜xOnA𝑜BOnA𝑜xA𝑜x+𝑜yA𝑜x+𝑜yA𝑜BA𝑜xA𝑜B
65 57 63 64 syl2anc AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜xA𝑜x+𝑜yA𝑜x+𝑜yA𝑜BA𝑜xA𝑜B
66 61 62 65 mp2and AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜xA𝑜B
67 simpllr AOnBOnA𝑜x+𝑜yA𝑜ByAxOnBOn
68 62 ne0d AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜B
69 on0eln0 A𝑜BOnA𝑜BA𝑜B
70 63 69 syl AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜BA𝑜B
71 68 70 mpbird AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜B
72 om00el AOnBOnA𝑜BAB
73 72 ad2antrr AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA𝑜BAB
74 71 73 mpbid AOnBOnA𝑜x+𝑜yA𝑜ByAxOnAB
75 74 simpld AOnBOnA𝑜x+𝑜yA𝑜ByAxOnA
76 omord2 xOnBOnAOnAxBA𝑜xA𝑜B
77 56 67 55 75 76 syl31anc AOnBOnA𝑜x+𝑜yA𝑜ByAxOnxBA𝑜xA𝑜B
78 66 77 mpbird AOnBOnA𝑜x+𝑜yA𝑜ByAxOnxB
79 78 ex AOnBOnA𝑜x+𝑜yA𝑜ByAxOnxB
80 54 79 impbid AOnBOnA𝑜x+𝑜yA𝑜ByAxBxOn
81 80 expr AOnBOnA𝑜x+𝑜yA𝑜ByAxBxOn
82 81 pm5.32rd AOnBOnA𝑜x+𝑜yA𝑜BxByAxOnyA
83 52 82 sylan2 AOnBOnmA𝑜Bm=A𝑜x+𝑜yxByAxOnyA
84 83 expr AOnBOnmA𝑜Bm=A𝑜x+𝑜yxByAxOnyA
85 84 pm5.32rd AOnBOnmA𝑜BxByAm=A𝑜x+𝑜yxOnyAm=A𝑜x+𝑜y
86 eqcom m=A𝑜x+𝑜yA𝑜x+𝑜y=m
87 86 anbi2i xOnyAm=A𝑜x+𝑜yxOnyAA𝑜x+𝑜y=m
88 85 87 bitrdi AOnBOnmA𝑜BxByAm=A𝑜x+𝑜yxOnyAA𝑜x+𝑜y=m
89 88 anbi2d AOnBOnmA𝑜Bn=xyxByAm=A𝑜x+𝑜yn=xyxOnyAA𝑜x+𝑜y=m
90 an12 n=xyxOnyAA𝑜x+𝑜y=mxOnyAn=xyA𝑜x+𝑜y=m
91 89 90 bitrdi AOnBOnmA𝑜Bn=xyxByAm=A𝑜x+𝑜yxOnyAn=xyA𝑜x+𝑜y=m
92 91 2exbidv AOnBOnmA𝑜Bxyn=xyxByAm=A𝑜x+𝑜yxyxOnyAn=xyA𝑜x+𝑜y=m
93 df-mpo xB,yAA𝑜x+𝑜y=xym|xByAm=A𝑜x+𝑜y
94 dfoprab2 xym|xByAm=A𝑜x+𝑜y=nm|xyn=xyxByAm=A𝑜x+𝑜y
95 1 93 94 3eqtri F=nm|xyn=xyxByAm=A𝑜x+𝑜y
96 95 breqi nFmnnm|xyn=xyxByAm=A𝑜x+𝑜ym
97 df-br nnm|xyn=xyxByAm=A𝑜x+𝑜ymnmnm|xyn=xyxByAm=A𝑜x+𝑜y
98 opabidw nmnm|xyn=xyxByAm=A𝑜x+𝑜yxyn=xyxByAm=A𝑜x+𝑜y
99 96 97 98 3bitri nFmxyn=xyxByAm=A𝑜x+𝑜y
100 r2ex xOnyAn=xyA𝑜x+𝑜y=mxyxOnyAn=xyA𝑜x+𝑜y=m
101 92 99 100 3bitr4g AOnBOnmA𝑜BnFmxOnyAn=xyA𝑜x+𝑜y=m
102 50 101 bitrid AOnBOnmA𝑜BmF-1nxOnyAn=xyA𝑜x+𝑜y=m
103 102 eubidv AOnBOnmA𝑜B∃!nmF-1n∃!nxOnyAn=xyA𝑜x+𝑜y=m
104 47 103 mpbird AOnBOnmA𝑜B∃!nmF-1n
105 104 ralrimiva AOnBOnmA𝑜B∃!nmF-1n
106 fnres F-1A𝑜BFnA𝑜BmA𝑜B∃!nmF-1n
107 105 106 sylibr AOnBOnF-1A𝑜BFnA𝑜B
108 relcnv RelF-1
109 df-rn ranF=domF-1
110 30 frnd AOnBOnranFA𝑜B
111 109 110 eqsstrrid AOnBOndomF-1A𝑜B
112 relssres RelF-1domF-1A𝑜BF-1A𝑜B=F-1
113 108 111 112 sylancr AOnBOnF-1A𝑜B=F-1
114 113 fneq1d AOnBOnF-1A𝑜BFnA𝑜BF-1FnA𝑜B
115 107 114 mpbid AOnBOnF-1FnA𝑜B
116 dff1o4 F:B×A1-1 ontoA𝑜BFFnB×AF-1FnA𝑜B
117 31 115 116 sylanbrc AOnBOnF:B×A1-1 ontoA𝑜B