Theorem djuun 6681

Description: The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.)

Assertion

Ref	Expression
djuun	|- ( (inl " A ) u. (inr " B ) ) = ( A ⊔ B )

Proof of Theorem djuun

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ima 4417	. . . 4 |- (inl " A ) = ran (inl |` A )
2		inlresf1 6674	. . . . 5 |- (inl |` A ) : A -1-1-> ( A ⊔ B )
3		f1rn 5168	. . . . 5 |- ( (inl |` A ) : A -1-1-> ( A ⊔ B ) -> ran (inl |` A ) C_ ( A ⊔ B ) )
4	2, 3	ax-mp 7	. . . 4 |- ran (inl |` A ) C_ ( A ⊔ B )
5	1, 4	eqsstri 3042	. . 3 |- (inl " A ) C_ ( A ⊔ B )
6		df-ima 4417	. . . 4 |- (inr " B ) = ran (inr |` B )
7		inrresf1 6675	. . . . 5 |- (inr |` B ) : B -1-1-> ( A ⊔ B )
8		f1rn 5168	. . . . 5 |- ( (inr |` B ) : B -1-1-> ( A ⊔ B ) -> ran (inr |` B ) C_ ( A ⊔ B ) )
9	7, 8	ax-mp 7	. . . 4 |- ran (inr |` B ) C_ ( A ⊔ B )
10	6, 9	eqsstri 3042	. . 3 |- (inr " B ) C_ ( A ⊔ B )
11	5, 10	unssi 3161	. 2 |- ( (inl " A ) u. (inr " B ) ) C_ ( A ⊔ B )
12		djur 6678	. . . . 5 |- ( x e. ( A ⊔ B ) -> ( E. y e. A x = (inl ` y ) \/ E. y e. B x = (inr ` y ) ) )
13		vex 2617	. . . . . . . . . 10 |- y e. _V
14		djulf1o 6671	. . . . . . . . . . 11 |- inl : _V -1-1-onto-> ( { (/) } X. _V )
15		f1odm 5208	. . . . . . . . . . 11 |- (inl : _V -1-1-onto-> ( { (/) } X. _V ) -> dom inl = _V )
16	14, 15	ax-mp 7	. . . . . . . . . 10 |- dom inl = _V
17	13, 16	eleqtrri 2160	. . . . . . . . 9 |- y e. dom inl
18		simpl 107	. . . . . . . . 9 |- ( ( y e. A /\ x = (inl ` y ) ) -> y e. A )
19		df-inl 6660	. . . . . . . . . . 11 |- inl = ( z e. _V |-> <. (/) , z >. )
20	19	funmpt2 5009	. . . . . . . . . 10 |- Fun inl
21		funfvima 5469	. . . . . . . . . 10 |- ( ( Fun inl /\ y e. dom inl ) -> ( y e. A -> (inl ` y ) e. (inl " A ) ) )
22	20, 21	mpan 415	. . . . . . . . 9 |- ( y e. dom inl -> ( y e. A -> (inl ` y ) e. (inl " A ) ) )
23	17, 18, 22	mpsyl 64	. . . . . . . 8 |- ( ( y e. A /\ x = (inl ` y ) ) -> (inl ` y ) e. (inl " A ) )
24		eleq1 2147	. . . . . . . . 9 |- ( x = (inl ` y ) -> ( x e. (inl " A ) <-> (inl ` y ) e. (inl " A ) ) )
25	24	adantl 271	. . . . . . . 8 |- ( ( y e. A /\ x = (inl ` y ) ) -> ( x e. (inl " A ) <-> (inl ` y ) e. (inl " A ) ) )
26	23, 25	mpbird 165	. . . . . . 7 |- ( ( y e. A /\ x = (inl ` y ) ) -> x e. (inl " A ) )
27	26	rexlimiva 2480	. . . . . 6 |- ( E. y e. A x = (inl ` y ) -> x e. (inl " A ) )
28		djurf1o 6672	. . . . . . . . . . 11 |- inr : _V -1-1-onto-> ( { 1o } X. _V )
29		f1odm 5208	. . . . . . . . . . 11 |- (inr : _V -1-1-onto-> ( { 1o } X. _V ) -> dom inr = _V )
30	28, 29	ax-mp 7	. . . . . . . . . 10 |- dom inr = _V
31	13, 30	eleqtrri 2160	. . . . . . . . 9 |- y e. dom inr
32		simpl 107	. . . . . . . . 9 |- ( ( y e. B /\ x = (inr ` y ) ) -> y e. B )
33		f1ofun 5206	. . . . . . . . . . 11 |- (inr : _V -1-1-onto-> ( { 1o } X. _V ) -> Fun inr )
34	28, 33	ax-mp 7	. . . . . . . . . 10 |- Fun inr
35		funfvima 5469	. . . . . . . . . 10 |- ( ( Fun inr /\ y e. dom inr ) -> ( y e. B -> (inr ` y ) e. (inr " B ) ) )
36	34, 35	mpan 415	. . . . . . . . 9 |- ( y e. dom inr -> ( y e. B -> (inr ` y ) e. (inr " B ) ) )
37	31, 32, 36	mpsyl 64	. . . . . . . 8 |- ( ( y e. B /\ x = (inr ` y ) ) -> (inr ` y ) e. (inr " B ) )
38		eleq1 2147	. . . . . . . . 9 |- ( x = (inr ` y ) -> ( x e. (inr " B ) <-> (inr ` y ) e. (inr " B ) ) )
39	38	adantl 271	. . . . . . . 8 |- ( ( y e. B /\ x = (inr ` y ) ) -> ( x e. (inr " B ) <-> (inr ` y ) e. (inr " B ) ) )
40	37, 39	mpbird 165	. . . . . . 7 |- ( ( y e. B /\ x = (inr ` y ) ) -> x e. (inr " B ) )
41	40	rexlimiva 2480	. . . . . 6 |- ( E. y e. B x = (inr ` y ) -> x e. (inr " B ) )
42	27, 41	orim12i 709	. . . . 5 |- ( ( E. y e. A x = (inl ` y ) \/ E. y e. B x = (inr ` y ) ) -> ( x e. (inl " A ) \/ x e. (inr " B ) ) )
43	12, 42	syl 14	. . . 4 |- ( x e. ( A ⊔ B ) -> ( x e. (inl " A ) \/ x e. (inr " B ) ) )
44		elun 3127	. . . 4 |- ( x e. ( (inl " A ) u. (inr " B ) ) <-> ( x e. (inl " A ) \/ x e. (inr " B ) ) )
45	43, 44	sylibr 132	. . 3 |- ( x e. ( A ⊔ B ) -> x e. ( (inl " A ) u. (inr " B ) ) )
46	45	ssriv 3016	. 2 |- ( A ⊔ B ) C_ ( (inl " A ) u. (inr " B ) )
47	11, 46	eqssi 3028	1 |- ( (inl " A ) u. (inr " B ) ) = ( A ⊔ B )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   \/ wo 662   = wceq 1287   e. wcel 1436   E.wrex 2356   _Vcvv 2614   u. cun 2984   C_ wss 2986   (/)c0 3272   {csn 3425   <.cop 3428   X. cxp 4402   dom cdm 4404   ran crn 4405   |` cres 4406   "cima 4407   Fun wfun 4966   -1-1->wf1 4969   -1-1-onto->wf1o 4971   ` cfv 4972   1oc1o 6109   ⊔ cdju 6651  inlcinl 6658  inrcinr 6659

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 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2616  df-sbc 2829  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-id 4087  df-iord 4160  df-on 4162  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-1st 5849  df-2nd 5850  df-1o 6116  df-dju 6652  df-inl 6660  df-inr 6661

This theorem is referenced by:  dju1p1e2  6744