Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  xmetxp Unicode version

Theorem xmetxp 12878
 Description: The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.)
Hypotheses
Ref Expression
xmetxp.p
xmetxp.1
xmetxp.2
Assertion
Ref Expression
xmetxp
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem xmetxp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xmetxp.1 . . . 4
2 eqid 2157 . . . . 5
32mopnm 12819 . . . 4
41, 3syl 14 . . 3
5 xmetxp.2 . . . 4
6 eqid 2157 . . . . 5
76mopnm 12819 . . . 4
85, 7syl 14 . . 3
9 xpexg 4699 . . 3
104, 8, 9syl2anc 409 . 2
111adantr 274 . . . . . 6
12 xp1st 6110 . . . . . . 7
1312ad2antrl 482 . . . . . 6
14 xp1st 6110 . . . . . . 7
1514ad2antll 483 . . . . . 6
16 xmetcl 12723 . . . . . 6
1711, 13, 15, 16syl3anc 1220 . . . . 5
185adantr 274 . . . . . 6
19 xp2nd 6111 . . . . . . 7
2019ad2antrl 482 . . . . . 6
21 xp2nd 6111 . . . . . . 7
2221ad2antll 483 . . . . . 6
23 xmetcl 12723 . . . . . 6
2418, 20, 22, 23syl3anc 1220 . . . . 5
25 xrmaxcl 11142 . . . . 5
2617, 24, 25syl2anc 409 . . . 4
2726ralrimivva 2539 . . 3
28 xmetxp.p . . . . 5
29 fveq2 5467 . . . . . . . . 9
3029oveq1d 5836 . . . . . . . 8
31 fveq2 5467 . . . . . . . . 9
3231oveq1d 5836 . . . . . . . 8
3330, 32preq12d 3644 . . . . . . 7
3433supeq1d 6927 . . . . . 6
35 fveq2 5467 . . . . . . . . 9
3635oveq2d 5837 . . . . . . . 8
37 fveq2 5467 . . . . . . . . 9
3837oveq2d 5837 . . . . . . . 8
3936, 38preq12d 3644 . . . . . . 7
4039supeq1d 6927 . . . . . 6
4134, 40cbvmpov 5898 . . . . 5
4228, 41eqtri 2178 . . . 4
4342fmpo 6146 . . 3
4427, 43sylib 121 . 2
45 simprl 521 . . . . . . . 8
46 simprr 522 . . . . . . . 8
4734, 40, 28ovmpog 5952 . . . . . . . 8
4845, 46, 26, 47syl3anc 1220 . . . . . . 7
4948, 26eqeltrd 2234 . . . . . 6
50 0xr 7918 . . . . . . 7
5150a1i 9 . . . . . 6
52 xrletri3 9702 . . . . . 6
5349, 51, 52syl2anc 409 . . . . 5
54 xmetge0 12736 . . . . . . . . 9
5511, 13, 15, 54syl3anc 1220 . . . . . . . 8
56 xrmax1sup 11143 . . . . . . . . 9
5717, 24, 56syl2anc 409 . . . . . . . 8
5851, 17, 26, 55, 57xrletrd 9709 . . . . . . 7
5958, 48breqtrrd 3992 . . . . . 6
6059biantrud 302 . . . . 5
6153, 60bitr4d 190 . . . 4
6248breq1d 3975 . . . 4
63 xrmaxlesup 11149 . . . . 5
6417, 24, 51, 63syl3anc 1220 . . . 4
6561, 62, 643bitrd 213 . . 3
6655biantrud 302 . . . . 5
67 xrletri3 9702 . . . . . 6
6817, 51, 67syl2anc 409 . . . . 5
6966, 68bitr4d 190 . . . 4
70 xmetge0 12736 . . . . . . 7
7118, 20, 22, 70syl3anc 1220 . . . . . 6
7271biantrud 302 . . . . 5
73 xrletri3 9702 . . . . . 6
7424, 51, 73syl2anc 409 . . . . 5
7572, 74bitr4d 190 . . . 4
7669, 75anbi12d 465 . . 3
77 xmeteq0 12730 . . . . . 6
7811, 13, 15, 77syl3anc 1220 . . . . 5
79 xmeteq0 12730 . . . . . 6
8018, 20, 22, 79syl3anc 1220 . . . . 5
8178, 80anbi12d 465 . . . 4
82 xpopth 6121 . . . . 5
8382adantl 275 . . . 4
8481, 83bitrd 187 . . 3
8565, 76, 843bitrd 213 . 2
87173adantr3 1143 . . . . 5
881adantr 274 . . . . . . 7
89 simpr3 990 . . . . . . . 8
90 xp1st 6110 . . . . . . . 8
9189, 90syl 14 . . . . . . 7
92 simpr1 988 . . . . . . . 8
9392, 12syl 14 . . . . . . 7
94 xmetcl 12723 . . . . . . 7
9588, 91, 93, 94syl3anc 1220 . . . . . 6
96153adantr3 1143 . . . . . . 7
97 xmetcl 12723 . . . . . . 7
9888, 91, 96, 97syl3anc 1220 . . . . . 6
9995, 98xaddcld 9781 . . . . 5
1005adantr 274 . . . . . . . . . 10
101 xp2nd 6111 . . . . . . . . . . 11
10289, 101syl 14 . . . . . . . . . 10
10392, 19syl 14 . . . . . . . . . 10
104 xmetcl 12723 . . . . . . . . . 10
105100, 102, 103, 104syl3anc 1220 . . . . . . . . 9
106 xrmaxcl 11142 . . . . . . . . 9
10795, 105, 106syl2anc 409 . . . . . . . 8
108 fveq2 5467 . . . . . . . . . . . 12
109 fveq2 5467 . . . . . . . . . . . 12
110108, 109oveqan12d 5840 . . . . . . . . . . 11
111 fveq2 5467 . . . . . . . . . . . 12
112 fveq2 5467 . . . . . . . . . . . 12
113111, 112oveqan12d 5840 . . . . . . . . . . 11
114110, 113preq12d 3644 . . . . . . . . . 10
115114supeq1d 6927 . . . . . . . . 9
116115, 28ovmpoga 5947 . . . . . . . 8
11789, 92, 107, 116syl3anc 1220 . . . . . . 7
118117, 107eqeltrd 2234 . . . . . 6
119 simpr2 989 . . . . . . . 8
120223adantr3 1143 . . . . . . . . . 10
121 xmetcl 12723 . . . . . . . . . 10
122100, 102, 120, 121syl3anc 1220 . . . . . . . . 9
123 xrmaxcl 11142 . . . . . . . . 9
12498, 122, 123syl2anc 409 . . . . . . . 8
125108, 35oveqan12d 5840 . . . . . . . . . . 11
126111, 37oveqan12d 5840 . . . . . . . . . . 11
127125, 126preq12d 3644 . . . . . . . . . 10
128127supeq1d 6927 . . . . . . . . 9
129128, 28ovmpoga 5947 . . . . . . . 8
13089, 119, 124, 129syl3anc 1220 . . . . . . 7
131130, 124eqeltrd 2234 . . . . . 6
132118, 131xaddcld 9781 . . . . 5
133 xmettri2 12732 . . . . . 6
13488, 91, 93, 96, 133syl13anc 1222 . . . . 5
135 xrmax1sup 11143 . . . . . . . 8
13695, 105, 135syl2anc 409 . . . . . . 7
137136, 117breqtrrd 3992 . . . . . 6
138 xrmax1sup 11143 . . . . . . . 8
13998, 122, 138syl2anc 409 . . . . . . 7
140139, 130breqtrrd 3992 . . . . . 6
141 xle2add 9776 . . . . . . 7
14295, 98, 118, 131, 141syl22anc 1221 . . . . . 6
143137, 140, 142mp2and 430 . . . . 5
14487, 99, 132, 134, 143xrletrd 9709 . . . 4
145243adantr3 1143 . . . . 5
146105, 122xaddcld 9781 . . . . 5
147 xmettri2 12732 . . . . . 6
148100, 102, 103, 120, 147syl13anc 1222 . . . . 5
149 xrmax2sup 11144 . . . . . . . 8
15095, 105, 149syl2anc 409 . . . . . . 7
151150, 117breqtrrd 3992 . . . . . 6
152 xrmax2sup 11144 . . . . . . . 8
15398, 122, 152syl2anc 409 . . . . . . 7
154153, 130breqtrrd 3992 . . . . . 6
155 xle2add 9776 . . . . . . 7
156105, 122, 118, 131, 155syl22anc 1221 . . . . . 6
157151, 154, 156mp2and 430 . . . . 5
158145, 146, 132, 148, 157xrletrd 9709 . . . 4
159 xrmaxlesup 11149 . . . . 5
16087, 145, 132, 159syl3anc 1220 . . . 4
161144, 158, 160mpbir2and 929 . . 3
16286, 161eqbrtrd 3986 . 2
16310, 44, 85, 162isxmetd 12718 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963   wceq 1335   wcel 2128  wral 2435  cvv 2712  cpr 3561   class class class wbr 3965   cxp 4583  wf 5165  cfv 5169  (class class class)co 5821   cmpo 5823  c1st 6083  c2nd 6084  csup 6922  cc0 7726  cxr 7905   clt 7906   cle 7907  cxad 9670  cxmet 12351  cmopn 12356 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-iinf 4546  ax-cnex 7817  ax-resscn 7818  ax-1cn 7819  ax-1re 7820  ax-icn 7821  ax-addcl 7822  ax-addrcl 7823  ax-mulcl 7824  ax-mulrcl 7825  ax-addcom 7826  ax-mulcom 7827  ax-addass 7828  ax-mulass 7829  ax-distr 7830  ax-i2m1 7831  ax-0lt1 7832  ax-1rid 7833  ax-0id 7834  ax-rnegex 7835  ax-precex 7836  ax-cnre 7837  ax-pre-ltirr 7838  ax-pre-ltwlin 7839  ax-pre-lttrn 7840  ax-pre-apti 7841  ax-pre-ltadd 7842  ax-pre-mulgt0 7843  ax-pre-mulext 7844  ax-arch 7845  ax-caucvg 7846 This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4253  df-po 4256  df-iso 4257  df-iord 4326  df-on 4328  df-ilim 4329  df-suc 4331  df-iom 4549  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-isom 5178  df-riota 5777  df-ov 5824  df-oprab 5825  df-mpo 5826  df-1st 6085  df-2nd 6086  df-recs 6249  df-frec 6335  df-map 6592  df-sup 6924  df-inf 6925  df-pnf 7908  df-mnf 7909  df-xr 7910  df-ltxr 7911  df-le 7912  df-sub 8042  df-neg 8043  df-reap 8444  df-ap 8451  df-div 8540  df-inn 8828  df-2 8886  df-3 8887  df-4 8888  df-n0 9085  df-z 9162  df-uz 9434  df-q 9522  df-rp 9554  df-xneg 9672  df-xadd 9673  df-seqfrec 10338  df-exp 10412  df-cj 10735  df-re 10736  df-im 10737  df-rsqrt 10891  df-abs 10892  df-topgen 12343  df-psmet 12358  df-xmet 12359  df-bl 12361  df-mopn 12362  df-top 12367  df-topon 12380  df-bases 12412 This theorem is referenced by:  xmetxpbl  12879  xmettxlem  12880  xmettx  12881  txmetcnp  12889
 Copyright terms: Public domain W3C validator