MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  znleval Structured version   Visualization version   GIF version

Theorem znleval 20619
Description: The ordering of the ℤ/n structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
Hypotheses
Ref Expression
znle2.y 𝑌 = (ℤ/nℤ‘𝑁)
znle2.f 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
znle2.w 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
znle2.l = (le‘𝑌)
znleval.x 𝑋 = (Base‘𝑌)
Assertion
Ref Expression
znleval (𝑁 ∈ ℕ0 → (𝐴 𝐵 ↔ (𝐴𝑋𝐵𝑋 ∧ (𝐹𝐴) ≤ (𝐹𝐵))))

Proof of Theorem znleval
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 znle2.y . . . . . . 7 𝑌 = (ℤ/nℤ‘𝑁)
2 znle2.f . . . . . . 7 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
3 znle2.w . . . . . . 7 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
4 znle2.l . . . . . . 7 = (le‘𝑌)
51, 2, 3, 4znle2 20618 . . . . . 6 (𝑁 ∈ ℕ0 = ((𝐹 ∘ ≤ ) ∘ 𝐹))
6 relco 6094 . . . . . . . 8 Rel ((𝐹 ∘ ≤ ) ∘ 𝐹)
7 relssdmrn 6118 . . . . . . . 8 (Rel ((𝐹 ∘ ≤ ) ∘ 𝐹) → ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ 𝐹) × ran ((𝐹 ∘ ≤ ) ∘ 𝐹)))
86, 7ax-mp 5 . . . . . . 7 ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ 𝐹) × ran ((𝐹 ∘ ≤ ) ∘ 𝐹))
9 dmcoss 5840 . . . . . . . . 9 dom ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ dom 𝐹
10 df-rn 5564 . . . . . . . . . 10 ran 𝐹 = dom 𝐹
11 znleval.x . . . . . . . . . . . 12 𝑋 = (Base‘𝑌)
121, 11, 2, 3znf1o 20616 . . . . . . . . . . 11 (𝑁 ∈ ℕ0𝐹:𝑊1-1-onto𝑋)
13 f1ofo 6618 . . . . . . . . . . 11 (𝐹:𝑊1-1-onto𝑋𝐹:𝑊onto𝑋)
14 forn 6589 . . . . . . . . . . 11 (𝐹:𝑊onto𝑋 → ran 𝐹 = 𝑋)
1512, 13, 143syl 18 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → ran 𝐹 = 𝑋)
1610, 15syl5eqr 2874 . . . . . . . . 9 (𝑁 ∈ ℕ0 → dom 𝐹 = 𝑋)
179, 16sseqtrid 4022 . . . . . . . 8 (𝑁 ∈ ℕ0 → dom ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ 𝑋)
18 rncoss 5841 . . . . . . . . 9 ran ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ ran (𝐹 ∘ ≤ )
19 rncoss 5841 . . . . . . . . . 10 ran (𝐹 ∘ ≤ ) ⊆ ran 𝐹
2019, 15sseqtrid 4022 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ran (𝐹 ∘ ≤ ) ⊆ 𝑋)
2118, 20sstrid 3981 . . . . . . . 8 (𝑁 ∈ ℕ0 → ran ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ 𝑋)
22 xpss12 5568 . . . . . . . 8 ((dom ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ 𝑋 ∧ ran ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ 𝑋) → (dom ((𝐹 ∘ ≤ ) ∘ 𝐹) × ran ((𝐹 ∘ ≤ ) ∘ 𝐹)) ⊆ (𝑋 × 𝑋))
2317, 21, 22syl2anc 584 . . . . . . 7 (𝑁 ∈ ℕ0 → (dom ((𝐹 ∘ ≤ ) ∘ 𝐹) × ran ((𝐹 ∘ ≤ ) ∘ 𝐹)) ⊆ (𝑋 × 𝑋))
248, 23sstrid 3981 . . . . . 6 (𝑁 ∈ ℕ0 → ((𝐹 ∘ ≤ ) ∘ 𝐹) ⊆ (𝑋 × 𝑋))
255, 24eqsstrd 4008 . . . . 5 (𝑁 ∈ ℕ0 ⊆ (𝑋 × 𝑋))
2625ssbrd 5105 . . . 4 (𝑁 ∈ ℕ0 → (𝐴 𝐵𝐴(𝑋 × 𝑋)𝐵))
27 brxp 5599 . . . 4 (𝐴(𝑋 × 𝑋)𝐵 ↔ (𝐴𝑋𝐵𝑋))
2826, 27syl6ib 252 . . 3 (𝑁 ∈ ℕ0 → (𝐴 𝐵 → (𝐴𝑋𝐵𝑋)))
2928pm4.71rd 563 . 2 (𝑁 ∈ ℕ0 → (𝐴 𝐵 ↔ ((𝐴𝑋𝐵𝑋) ∧ 𝐴 𝐵)))
305adantr 481 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → = ((𝐹 ∘ ≤ ) ∘ 𝐹))
3130breqd 5073 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝐴 𝐵𝐴((𝐹 ∘ ≤ ) ∘ 𝐹)𝐵))
32 brcog 5735 . . . . . . 7 ((𝐴𝑋𝐵𝑋) → (𝐴((𝐹 ∘ ≤ ) ∘ 𝐹)𝐵 ↔ ∃𝑥(𝐴𝐹𝑥𝑥(𝐹 ∘ ≤ )𝐵)))
3332adantl 482 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ 𝐹)𝐵 ↔ ∃𝑥(𝐴𝐹𝑥𝑥(𝐹 ∘ ≤ )𝐵)))
34 eqcom 2832 . . . . . . . . 9 (𝑥 = (𝐹𝐴) ↔ (𝐹𝐴) = 𝑥)
3512adantr 481 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → 𝐹:𝑊1-1-onto𝑋)
36 f1ocnv 6623 . . . . . . . . . . 11 (𝐹:𝑊1-1-onto𝑋𝐹:𝑋1-1-onto𝑊)
37 f1ofn 6612 . . . . . . . . . . 11 (𝐹:𝑋1-1-onto𝑊𝐹 Fn 𝑋)
3835, 36, 373syl 18 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → 𝐹 Fn 𝑋)
39 simprl 767 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → 𝐴𝑋)
40 fnbrfvb 6714 . . . . . . . . . 10 ((𝐹 Fn 𝑋𝐴𝑋) → ((𝐹𝐴) = 𝑥𝐴𝐹𝑥))
4138, 39, 40syl2anc 584 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) = 𝑥𝐴𝐹𝑥))
4234, 41syl5rbb 285 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐹𝑥𝑥 = (𝐹𝐴)))
4342anbi1d 629 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐹𝑥𝑥(𝐹 ∘ ≤ )𝐵) ↔ (𝑥 = (𝐹𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
4443exbidv 1915 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (∃𝑥(𝐴𝐹𝑥𝑥(𝐹 ∘ ≤ )𝐵) ↔ ∃𝑥(𝑥 = (𝐹𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
4533, 44bitrd 280 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ 𝐹)𝐵 ↔ ∃𝑥(𝑥 = (𝐹𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
46 fvex 6679 . . . . . . 7 (𝐹𝐴) ∈ V
47 breq1 5065 . . . . . . 7 (𝑥 = (𝐹𝐴) → (𝑥(𝐹 ∘ ≤ )𝐵 ↔ (𝐹𝐴)(𝐹 ∘ ≤ )𝐵))
4846, 47ceqsexv 3546 . . . . . 6 (∃𝑥(𝑥 = (𝐹𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (𝐹𝐴)(𝐹 ∘ ≤ )𝐵)
49 simprr 769 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → 𝐵𝑋)
50 brcog 5735 . . . . . . . 8 (((𝐹𝐴) ∈ V ∧ 𝐵𝑋) → ((𝐹𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((𝐹𝐴) ≤ 𝑥𝑥𝐹𝐵)))
5146, 49, 50sylancr 587 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((𝐹𝐴) ≤ 𝑥𝑥𝐹𝐵)))
52 fvex 6679 . . . . . . . . 9 (𝐹𝐵) ∈ V
53 breq2 5066 . . . . . . . . 9 (𝑥 = (𝐹𝐵) → ((𝐹𝐴) ≤ 𝑥 ↔ (𝐹𝐴) ≤ (𝐹𝐵)))
5452, 53ceqsexv 3546 . . . . . . . 8 (∃𝑥(𝑥 = (𝐹𝐵) ∧ (𝐹𝐴) ≤ 𝑥) ↔ (𝐹𝐴) ≤ (𝐹𝐵))
55 eqcom 2832 . . . . . . . . . . . . 13 (𝑥 = (𝐹𝐵) ↔ (𝐹𝐵) = 𝑥)
56 fnbrfvb 6714 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋𝐵𝑋) → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥))
5738, 49, 56syl2anc 584 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐵) = 𝑥𝐵𝐹𝑥))
5855, 57syl5bb 284 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝑥 = (𝐹𝐵) ↔ 𝐵𝐹𝑥))
59 vex 3502 . . . . . . . . . . . . 13 𝑥 ∈ V
60 brcnvg 5748 . . . . . . . . . . . . 13 ((𝐵𝑋𝑥 ∈ V) → (𝐵𝐹𝑥𝑥𝐹𝐵))
6149, 59, 60sylancl 586 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝐵𝐹𝑥𝑥𝐹𝐵))
6258, 61bitrd 280 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝑥 = (𝐹𝐵) ↔ 𝑥𝐹𝐵))
6362anbi1d 629 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝑥 = (𝐹𝐵) ∧ (𝐹𝐴) ≤ 𝑥) ↔ (𝑥𝐹𝐵 ∧ (𝐹𝐴) ≤ 𝑥)))
6463biancomd 464 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝑥 = (𝐹𝐵) ∧ (𝐹𝐴) ≤ 𝑥) ↔ ((𝐹𝐴) ≤ 𝑥𝑥𝐹𝐵)))
6564exbidv 1915 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (∃𝑥(𝑥 = (𝐹𝐵) ∧ (𝐹𝐴) ≤ 𝑥) ↔ ∃𝑥((𝐹𝐴) ≤ 𝑥𝑥𝐹𝐵)))
6654, 65syl5bbr 286 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) ≤ (𝐹𝐵) ↔ ∃𝑥((𝐹𝐴) ≤ 𝑥𝑥𝐹𝐵)))
6751, 66bitr4d 283 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴)(𝐹 ∘ ≤ )𝐵 ↔ (𝐹𝐴) ≤ (𝐹𝐵)))
6848, 67syl5bb 284 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (∃𝑥(𝑥 = (𝐹𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (𝐹𝐴) ≤ (𝐹𝐵)))
6931, 45, 683bitrd 306 . . . 4 ((𝑁 ∈ ℕ0 ∧ (𝐴𝑋𝐵𝑋)) → (𝐴 𝐵 ↔ (𝐹𝐴) ≤ (𝐹𝐵)))
7069pm5.32da 579 . . 3 (𝑁 ∈ ℕ0 → (((𝐴𝑋𝐵𝑋) ∧ 𝐴 𝐵) ↔ ((𝐴𝑋𝐵𝑋) ∧ (𝐹𝐴) ≤ (𝐹𝐵))))
71 df-3an 1083 . . 3 ((𝐴𝑋𝐵𝑋 ∧ (𝐹𝐴) ≤ (𝐹𝐵)) ↔ ((𝐴𝑋𝐵𝑋) ∧ (𝐹𝐴) ≤ (𝐹𝐵)))
7270, 71syl6bbr 290 . 2 (𝑁 ∈ ℕ0 → (((𝐴𝑋𝐵𝑋) ∧ 𝐴 𝐵) ↔ (𝐴𝑋𝐵𝑋 ∧ (𝐹𝐴) ≤ (𝐹𝐵))))
7329, 72bitrd 280 1 (𝑁 ∈ ℕ0 → (𝐴 𝐵 ↔ (𝐴𝑋𝐵𝑋 ∧ (𝐹𝐴) ≤ (𝐹𝐵))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wex 1773  wcel 2107  Vcvv 3499  wss 3939  ifcif 4469   class class class wbr 5062   × cxp 5551  ccnv 5552  dom cdm 5553  ran crn 5554  cres 5555  ccom 5557  Rel wrel 5558   Fn wfn 6346  ontowfo 6349  1-1-ontowf1o 6350  cfv 6351  (class class class)co 7151  0cc0 10529  cle 10668  0cn0 11889  cz 11973  ..^cfzo 13026  Basecbs 16475  lecple 16564  ℤRHomczrh 20565  ℤ/nczn 20568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-tpos 7886  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-ec 8284  df-qs 8288  df-map 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12383  df-fz 12886  df-fzo 13027  df-fl 13155  df-mod 13231  df-seq 13363  df-dvds 15600  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-0g 16707  df-imas 16773  df-qus 16774  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-mhm 17946  df-grp 18038  df-minusg 18039  df-sbg 18040  df-mulg 18157  df-subg 18208  df-nsg 18209  df-eqg 18210  df-ghm 18288  df-cmn 18830  df-abl 18831  df-mgp 19162  df-ur 19174  df-ring 19221  df-cring 19222  df-oppr 19295  df-dvdsr 19313  df-rnghom 19389  df-subrg 19455  df-lmod 19558  df-lss 19626  df-lsp 19666  df-sra 19866  df-rgmod 19867  df-lidl 19868  df-rsp 19869  df-2idl 19926  df-cnfld 20464  df-zring 20536  df-zrh 20569  df-zn 20572
This theorem is referenced by:  znleval2  20620
  Copyright terms: Public domain W3C validator