MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  soisores Unicode version

Theorem soisores 6223
Description: Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015.)
Assertion
Ref Expression
soisores
Distinct variable groups:   , ,   , ,   , ,   ,S,

Proof of Theorem soisores
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isorel 6222 . . . . 5
2 fvres 5885 . . . . . . 7
3 fvres 5885 . . . . . . 7
42, 3breqan12d 4467 . . . . . 6
54adantl 466 . . . . 5
61, 5bitrd 253 . . . 4
76biimpd 207 . . 3
87ralrimivva 2878 . 2
9 ffn 5736 . . . . . . . 8
109ad2antrl 727 . . . . . . 7
11 simprr 757 . . . . . . 7
12 fnssres 5699 . . . . . . 7
1310, 11, 12syl2anc 661 . . . . . 6
14133adant3 1016 . . . . 5
15 df-ima 5017 . . . . . . 7
1615eqcomi 2470 . . . . . 6
1716a1i 11 . . . . 5
18 fvres 5885 . . . . . . . . 9
19 fvres 5885 . . . . . . . . 9
2018, 19eqeqan12d 2480 . . . . . . . 8
2120adantl 466 . . . . . . 7
22 simprl 756 . . . . . . . . . . 11
23 simprr 757 . . . . . . . . . . 11
24 simpl3 1001 . . . . . . . . . . 11
25 breq1 4455 . . . . . . . . . . . . 13
26 fveq2 5871 . . . . . . . . . . . . . 14
2726breq1d 4462 . . . . . . . . . . . . 13
2825, 27imbi12d 320 . . . . . . . . . . . 12
29 breq2 4456 . . . . . . . . . . . . 13
30 fveq2 5871 . . . . . . . . . . . . . 14
3130breq2d 4464 . . . . . . . . . . . . 13
3229, 31imbi12d 320 . . . . . . . . . . . 12
3328, 32rspc2va 3220 . . . . . . . . . . 11
3422, 23, 24, 33syl21anc 1227 . . . . . . . . . 10
35 breq1 4455 . . . . . . . . . . . . 13
36 fveq2 5871 . . . . . . . . . . . . . 14
3736breq1d 4462 . . . . . . . . . . . . 13
3835, 37imbi12d 320 . . . . . . . . . . . 12
39 breq2 4456 . . . . . . . . . . . . 13
40 fveq2 5871 . . . . . . . . . . . . . 14
4140breq2d 4464 . . . . . . . . . . . . 13
4239, 41imbi12d 320 . . . . . . . . . . . 12
4338, 42rspc2va 3220 . . . . . . . . . . 11
4423, 22, 24, 43syl21anc 1227 . . . . . . . . . 10
4534, 44orim12d 838 . . . . . . . . 9
4645con3d 133 . . . . . . . 8
47 simpl1r 1048 . . . . . . . . 9
48 simpl2l 1049 . . . . . . . . . 10
49 simpl2r 1050 . . . . . . . . . . 11
5049, 22sseldd 3504 . . . . . . . . . 10
5148, 50ffvelrnd 6032 . . . . . . . . 9
5249, 23sseldd 3504 . . . . . . . . . 10
5348, 52ffvelrnd 6032 . . . . . . . . 9
54 sotrieq 4832 . . . . . . . . 9
5547, 51, 53, 54syl12anc 1226 . . . . . . . 8
56 simpl1l 1047 . . . . . . . . 9
57 sotrieq 4832 . . . . . . . . 9
5856, 50, 52, 57syl12anc 1226 . . . . . . . 8
5946, 55, 583imtr4d 268 . . . . . . 7
6021, 59sylbid 215 . . . . . 6
6160ralrimivva 2878 . . . . 5
62 dff1o6 6181 . . . . 5
6314, 17, 61, 62syl3anbrc 1180 . . . 4
64 fveq2 5871 . . . . . . . . . . 11
6564a1i 11 . . . . . . . . . 10
6665, 44orim12d 838 . . . . . . . . 9
6766con3d 133 . . . . . . . 8
68 sotric 4831 . . . . . . . . 9
6947, 51, 53, 68syl12anc 1226 . . . . . . . 8
70 sotric 4831 . . . . . . . . 9
7156, 50, 52, 70syl12anc 1226 . . . . . . . 8
7267, 69, 713imtr4d 268 . . . . . . 7
7334, 72impbid 191 . . . . . 6
7418, 19breqan12d 4467 . . . . . . 7
7574adantl 466 . . . . . 6
7673, 75bitr4d 256 . . . . 5
7776ralrimivva 2878 . . . 4
78 df-isom 5602 . . . 4
7963, 77, 78sylanbrc 664 . . 3
80793expia 1198 . 2
818, 80impbid2 204 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  A.wral 2807  C_wss 3475   class class class wbr 4452  Orwor 4804  rancrn 5005  |`cres 5006  "cima 5007  Fnwfn 5588  -->wf 5589  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594
This theorem is referenced by:  isercolllem1  13487  dvgt0lem2  22404  erdszelem4  28638  erdszelem8  28642  erdsze2lem2  28648
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602
  Copyright terms: Public domain W3C validator