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

Theorem caseinj 6940
 Description: The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
Hypotheses
Ref Expression
caseinj.r
caseinj.s
caseinj.disj
Assertion
Ref Expression
caseinj case

Proof of Theorem caseinj
StepHypRef Expression
1 df-inl 6898 . . . . . . 7 inl
21funmpt2 5130 . . . . . 6 inl
3 funcnvcnv 5150 . . . . . 6 inl inl
42, 3ax-mp 5 . . . . 5 inl
5 caseinj.r . . . . 5
6 funco 5131 . . . . 5 inl inl
74, 5, 6sylancr 408 . . . 4 inl
8 cnvco 4692 . . . . 5 inl inl
98funeqi 5112 . . . 4 inl inl
107, 9sylibr 133 . . 3 inl
11 df-inr 6899 . . . . . . 7 inr
1211funmpt2 5130 . . . . . 6 inr
13 funcnvcnv 5150 . . . . . 6 inr inr
1412, 13ax-mp 5 . . . . 5 inr
15 caseinj.s . . . . 5
16 funco 5131 . . . . 5 inr inr
1714, 15, 16sylancr 408 . . . 4 inr
18 cnvco 4692 . . . . 5 inr inr
1918funeqi 5112 . . . 4 inr inr
2017, 19sylibr 133 . . 3 inr
21 df-rn 4518 . . . . . . 7 inl inl
22 rncoss 4777 . . . . . . 7 inl
2321, 22eqsstrri 3098 . . . . . 6 inl
24 df-rn 4518 . . . . . . 7 inr inr
25 rncoss 4777 . . . . . . 7 inr
2624, 25eqsstrri 3098 . . . . . 6 inr
27 ss2in 3272 . . . . . 6 inl inr inl inr
2823, 26, 27mp2an 420 . . . . 5 inl inr
29 caseinj.disj . . . . 5
3028, 29sseqtrid 3115 . . . 4 inl inr
31 ss0 3371 . . . 4 inl inr inl inr
3230, 31syl 14 . . 3 inl inr
33 funun 5135 . . 3 inl inr inl inr inl inr
3410, 20, 32, 33syl21anc 1198 . 2 inl inr
35 df-case 6935 . . . . 5 case inl inr
3635cnveqi 4682 . . . 4 case inl inr
37 cnvun 4912 . . . 4 inl inr inl inr
3836, 37eqtri 2136 . . 3 case inl inr
3938funeqi 5112 . 2 case inl inr
4034, 39sylibr 133 1 case
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1314  cvv 2658   cun 3037   cin 3038   wss 3039  c0 3331  cop 3498  ccnv 4506   cdm 4507   crn 4508   ccom 4511   wfun 5085  c1o 6272  inlcinl 6896  inrcinr 6897  casecdjucase 6934 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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099 This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-br 3898  df-opab 3958  df-mpt 3959  df-id 4183  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-fun 5093  df-inl 6898  df-inr 6899  df-case 6935 This theorem is referenced by:  casef1  6941
 Copyright terms: Public domain W3C validator