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

Theorem caseinj 6974
 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 (𝜑 → Fun 𝑅)
caseinj.s (𝜑 → Fun 𝑆)
caseinj.disj (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅)
Assertion
Ref Expression
caseinj (𝜑 → Fun case(𝑅, 𝑆))

Proof of Theorem caseinj
StepHypRef Expression
1 df-inl 6932 . . . . . . 7 inl = (𝑦 ∈ V ↦ ⟨∅, 𝑦⟩)
21funmpt2 5162 . . . . . 6 Fun inl
3 funcnvcnv 5182 . . . . . 6 (Fun inl → Fun inl)
42, 3ax-mp 5 . . . . 5 Fun inl
5 caseinj.r . . . . 5 (𝜑 → Fun 𝑅)
6 funco 5163 . . . . 5 ((Fun inl ∧ Fun 𝑅) → Fun (inl ∘ 𝑅))
74, 5, 6sylancr 410 . . . 4 (𝜑 → Fun (inl ∘ 𝑅))
8 cnvco 4724 . . . . 5 (𝑅inl) = (inl ∘ 𝑅)
98funeqi 5144 . . . 4 (Fun (𝑅inl) ↔ Fun (inl ∘ 𝑅))
107, 9sylibr 133 . . 3 (𝜑 → Fun (𝑅inl))
11 df-inr 6933 . . . . . . 7 inr = (𝑥 ∈ V ↦ ⟨1o, 𝑥⟩)
1211funmpt2 5162 . . . . . 6 Fun inr
13 funcnvcnv 5182 . . . . . 6 (Fun inr → Fun inr)
1412, 13ax-mp 5 . . . . 5 Fun inr
15 caseinj.s . . . . 5 (𝜑 → Fun 𝑆)
16 funco 5163 . . . . 5 ((Fun inr ∧ Fun 𝑆) → Fun (inr ∘ 𝑆))
1714, 15, 16sylancr 410 . . . 4 (𝜑 → Fun (inr ∘ 𝑆))
18 cnvco 4724 . . . . 5 (𝑆inr) = (inr ∘ 𝑆)
1918funeqi 5144 . . . 4 (Fun (𝑆inr) ↔ Fun (inr ∘ 𝑆))
2017, 19sylibr 133 . . 3 (𝜑 → Fun (𝑆inr))
21 df-rn 4550 . . . . . . 7 ran (𝑅inl) = dom (𝑅inl)
22 rncoss 4809 . . . . . . 7 ran (𝑅inl) ⊆ ran 𝑅
2321, 22eqsstrri 3130 . . . . . 6 dom (𝑅inl) ⊆ ran 𝑅
24 df-rn 4550 . . . . . . 7 ran (𝑆inr) = dom (𝑆inr)
25 rncoss 4809 . . . . . . 7 ran (𝑆inr) ⊆ ran 𝑆
2624, 25eqsstrri 3130 . . . . . 6 dom (𝑆inr) ⊆ ran 𝑆
27 ss2in 3304 . . . . . 6 ((dom (𝑅inl) ⊆ ran 𝑅 ∧ dom (𝑆inr) ⊆ ran 𝑆) → (dom (𝑅inl) ∩ dom (𝑆inr)) ⊆ (ran 𝑅 ∩ ran 𝑆))
2823, 26, 27mp2an 422 . . . . 5 (dom (𝑅inl) ∩ dom (𝑆inr)) ⊆ (ran 𝑅 ∩ ran 𝑆)
29 caseinj.disj . . . . 5 (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅)
3028, 29sseqtrid 3147 . . . 4 (𝜑 → (dom (𝑅inl) ∩ dom (𝑆inr)) ⊆ ∅)
31 ss0 3403 . . . 4 ((dom (𝑅inl) ∩ dom (𝑆inr)) ⊆ ∅ → (dom (𝑅inl) ∩ dom (𝑆inr)) = ∅)
3230, 31syl 14 . . 3 (𝜑 → (dom (𝑅inl) ∩ dom (𝑆inr)) = ∅)
33 funun 5167 . . 3 (((Fun (𝑅inl) ∧ Fun (𝑆inr)) ∧ (dom (𝑅inl) ∩ dom (𝑆inr)) = ∅) → Fun ((𝑅inl) ∪ (𝑆inr)))
3410, 20, 32, 33syl21anc 1215 . 2 (𝜑 → Fun ((𝑅inl) ∪ (𝑆inr)))
35 df-case 6969 . . . . 5 case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))
3635cnveqi 4714 . . . 4 case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))
37 cnvun 4944 . . . 4 ((𝑅inl) ∪ (𝑆inr)) = ((𝑅inl) ∪ (𝑆inr))
3836, 37eqtri 2160 . . 3 case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))
3938funeqi 5144 . 2 (Fun case(𝑅, 𝑆) ↔ Fun ((𝑅inl) ∪ (𝑆inr)))
4034, 39sylibr 133 1 (𝜑 → Fun case(𝑅, 𝑆))
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1331  Vcvv 2686   ∪ cun 3069   ∩ cin 3070   ⊆ wss 3071  ∅c0 3363  ⟨cop 3530  ◡ccnv 4538  dom cdm 4539  ran crn 4540   ∘ ccom 4543  Fun wfun 5117  1oc1o 6306  inlcinl 6930  inrcinr 6931  casecdjucase 6968 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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-fun 5125  df-inl 6932  df-inr 6933  df-case 6969 This theorem is referenced by:  casef1  6975
 Copyright terms: Public domain W3C validator