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

Theorem djur 6736
 Description: A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.)
Assertion
Ref Expression
djur inl inr
Distinct variable groups:   ,   ,   ,

Proof of Theorem djur
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-dju 6710 . . . 4
21eleq2i 2154 . . 3
3 elun 3139 . . 3
42, 3sylbb 121 . 2
5 xp2nd 5919 . . . 4
6 1st2nd2 5927 . . . . . 6
7 xp1st 5918 . . . . . . 7
8 elsni 3459 . . . . . . 7
9 opeq1 3617 . . . . . . . 8
109eqeq2d 2099 . . . . . . 7
117, 8, 103syl 17 . . . . . 6
126, 11mpbid 145 . . . . 5
13 2ndexg 5921 . . . . . 6
14 0ex 3958 . . . . . . 7
15 opexg 4046 . . . . . . 7
1614, 13, 15sylancr 405 . . . . . 6
17 opeq2 3618 . . . . . . 7
18 df-inl 6718 . . . . . . 7 inl
1917, 18fvmptg 5364 . . . . . 6 inl
2013, 16, 19syl2anc 403 . . . . 5 inl
2112, 20eqtr4d 2123 . . . 4 inl
22 fveq2 5289 . . . . . 6 inl inl
2322eqeq2d 2099 . . . . 5 inl inl
2423rspcev 2722 . . . 4 inl inl
255, 21, 24syl2anc 403 . . 3 inl
26 xp2nd 5919 . . . 4
27 1st2nd2 5927 . . . . . 6
28 xp1st 5918 . . . . . . 7
29 elsni 3459 . . . . . . 7
30 opeq1 3617 . . . . . . . 8
3130eqeq2d 2099 . . . . . . 7
3228, 29, 313syl 17 . . . . . 6
3327, 32mpbid 145 . . . . 5
34 2ndexg 5921 . . . . . 6
35 1onn 6259 . . . . . . 7
36 opexg 4046 . . . . . . 7
3735, 34, 36sylancr 405 . . . . . 6
38 opeq2 3618 . . . . . . 7
39 df-inr 6719 . . . . . . 7 inr
4038, 39fvmptg 5364 . . . . . 6 inr
4134, 37, 40syl2anc 403 . . . . 5 inr
4233, 41eqtr4d 2123 . . . 4 inr
43 fveq2 5289 . . . . . 6 inr inr
4443eqeq2d 2099 . . . . 5 inr inr
4544rspcev 2722 . . . 4 inr inr
4626, 42, 45syl2anc 403 . . 3 inr
4725, 46orim12i 711 . 2 inl inr
484, 47syl 14 1 inl inr
 Colors of variables: wff set class Syntax hints:   wi 4   wb 103   wo 664   wceq 1289   wcel 1438  wrex 2360  cvv 2619   cun 2995  c0 3284  csn 3441  cop 3444  com 4395   cxp 4426  cfv 5002  c1st 5891  c2nd 5892  c1o 6156   ⊔ cdju 6709  inlcinl 6716  inrcinr 6717 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251 This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-sbc 2839  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-br 3838  df-opab 3892  df-mpt 3893  df-id 4111  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-fo 5008  df-fv 5010  df-1st 5893  df-2nd 5894  df-1o 6163  df-dju 6710  df-inl 6718  df-inr 6719 This theorem is referenced by:  djuun  6739  djuss  6740  updjud  6752  fodjuomnilemdc  6778  exmidfodomrlemeldju  6804
 Copyright terms: Public domain W3C validator