updjud - Intuitionistic Logic Explorer

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

Theorem updjud 6960

Description: Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)

**Hypotheses**
Ref	Expression
updjud.f
updjud.g
updjud.a
updjud.b

**Assertion**
Ref	Expression
updjud	⊔ $/\$ inl $/\$ inr

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem updjud Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		updjud.a	. . . . . 6
2		updjud.b	. . . . . 6
3	1, 2	jca 304	. . . . 5 $/\$
4		djuex 6921	. . . . 5 $/\$ ⊔
5		mptexg 5638	. . . . 5 ⊔ ⊔
6	3, 4, 5	3syl 17	. . . 4 ⊔
7		feq1 5250	. . . . . . 7 ⊔ ⊔ ⊔ ⊔
8		coeq1 4691	. . . . . . . 8 ⊔ inl ⊔ inl
9	8	eqeq1d 2146	. . . . . . 7 ⊔ inl ⊔ inl
10		coeq1 4691	. . . . . . . 8 ⊔ inr ⊔ inr
11	10	eqeq1d 2146	. . . . . . 7 ⊔ inr ⊔ inr
12	7, 9, 11	3anbi123d 1290	. . . . . 6 ⊔ ⊔ $/\$ inl $/\$ inr ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr
13		eqeq1 2144	. . . . . . . 8 ⊔ ⊔
14	13	imbi2d 229	. . . . . . 7 ⊔ ⊔ $/\$ inl $/\$ inr ⊔ $/\$ inl $/\$ inr ⊔
15	14	ralbidv 2435	. . . . . 6 ⊔ ⊔ $/\$ inl $/\$ inr ⊔ $/\$ inl $/\$ inr ⊔
16	12, 15	anbi12d 464	. . . . 5 ⊔ ⊔ $/\$ inl $/\$ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
17	16	adantl 275	. . . 4 $/\$ ⊔ ⊔ $/\$ inl $/\$ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
18		updjud.f	. . . . . 6
19		updjud.g	. . . . . 6
20		eqid 2137	. . . . . 6 ⊔ ⊔
21	18, 19, 20	updjudhf 6957	. . . . 5 ⊔ ⊔
22	18, 19, 20	updjudhcoinlf 6958	. . . . 5 ⊔ inl
23	18, 19, 20	updjudhcoinrg 6959	. . . . 5 ⊔ inr
24		simpr 109	. . . . . . 7 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr
25		eqeq2 2147	. . . . . . . . . . . . . . . . . . . . . 22 ⊔ inl inl ⊔ inl inl
26		fvres 5438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 inl inl
27	26	eqcomd 2143	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 inl inl
28	27	eqeq2d 2149	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 inl inl
29	28	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊔ inl inl $/\$ $/\$ inl inl
30		fveq1 5413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊔ inl inl ⊔ inl inl
31	30	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊔ inl inl $/\$ $/\$ ⊔ inl inl
32		inlresf1 6939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 inl ⊔
33		f1fn 5325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 inl ⊔ inl
34	32, 33	mp1i 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊔ inl inl $/\$ inl
35		fvco2 5483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 inl $/\$ ⊔ inl ⊔ inl
36	34, 35	sylan 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊔ inl inl $/\$ $/\$ ⊔ inl ⊔ inl
37		fvco2 5483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 inl $/\$ inl inl
38	34, 37	sylan 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊔ inl inl $/\$ $/\$ inl inl
39	31, 36, 38	3eqtr3d 2178	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊔ inl inl $/\$ $/\$ ⊔ inl inl
40		fveq2 5414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 inl ⊔ ⊔ inl
41		fveq2 5414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 inl inl
42	40, 41	eqeq12d 2152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 inl ⊔ ⊔ inl inl
43	39, 42	syl5ibrcom 156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊔ inl inl $/\$ $/\$ inl ⊔
44	29, 43	sylbid 149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊔ inl inl $/\$ $/\$ inl ⊔
45	44	expimpd 360	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊔ inl inl $/\$ $/\$ inl ⊔
46	45	ex 114	. . . . . . . . . . . . . . . . . . . . . . 23 ⊔ inl inl $/\$ inl ⊔
47	46	eqcoms 2140	. . . . . . . . . . . . . . . . . . . . . 22 inl ⊔ inl $/\$ inl ⊔
48	25, 47	syl6bir 163	. . . . . . . . . . . . . . . . . . . . 21 ⊔ inl inl $/\$ inl ⊔
49	48	com23 78	. . . . . . . . . . . . . . . . . . . 20 ⊔ inl inl $/\$ inl ⊔
50	49	3ad2ant2 1003	. . . . . . . . . . . . . . . . . . 19 ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr inl $/\$ inl ⊔
51	50	impcom 124	. . . . . . . . . . . . . . . . . 18 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr inl $/\$ inl ⊔
52	51	com12 30	. . . . . . . . . . . . . . . . 17 inl $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ inl ⊔
53	52	3ad2ant2 1003	. . . . . . . . . . . . . . . 16 ⊔ $/\$ inl $/\$ inr $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ inl ⊔
54	53	impcom 124	. . . . . . . . . . . . . . 15 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr $/\$ inl ⊔
55	54	com12 30	. . . . . . . . . . . . . 14 $/\$ inl $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
56	55	rexlimiva 2542	. . . . . . . . . . . . 13 inl $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
57		eqeq2 2147	. . . . . . . . . . . . . . . . . . . . . 22 ⊔ inr inr ⊔ inr inr
58		fvres 5438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 inr inr
59	58	eqcomd 2143	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 inr inr
60	59	eqeq2d 2149	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 inr inr
61	60	adantl 275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊔ inr inr $/\$ $/\$ inr inr
62		fveq1 5413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊔ inr inr ⊔ inr inr
63	62	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊔ inr inr $/\$ $/\$ ⊔ inr inr
64		inrresf1 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 inr ⊔
65		f1fn 5325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 inr ⊔ inr
66	64, 65	mp1i 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊔ inr inr $/\$ inr
67		fvco2 5483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 inr $/\$ ⊔ inr ⊔ inr
68	66, 67	sylan 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊔ inr inr $/\$ $/\$ ⊔ inr ⊔ inr
69		fvco2 5483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 inr $/\$ inr inr
70	66, 69	sylan 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊔ inr inr $/\$ $/\$ inr inr
71	63, 68, 70	3eqtr3d 2178	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊔ inr inr $/\$ $/\$ ⊔ inr inr
72		fveq2 5414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 inr ⊔ ⊔ inr
73		fveq2 5414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 inr inr
74	72, 73	eqeq12d 2152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 inr ⊔ ⊔ inr inr
75	71, 74	syl5ibrcom 156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊔ inr inr $/\$ $/\$ inr ⊔
76	61, 75	sylbid 149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊔ inr inr $/\$ $/\$ inr ⊔
77	76	expimpd 360	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊔ inr inr $/\$ $/\$ inr ⊔
78	77	ex 114	. . . . . . . . . . . . . . . . . . . . . . 23 ⊔ inr inr $/\$ inr ⊔
79	78	eqcoms 2140	. . . . . . . . . . . . . . . . . . . . . 22 inr ⊔ inr $/\$ inr ⊔
80	57, 79	syl6bir 163	. . . . . . . . . . . . . . . . . . . . 21 ⊔ inr inr $/\$ inr ⊔
81	80	com23 78	. . . . . . . . . . . . . . . . . . . 20 ⊔ inr inr $/\$ inr ⊔
82	81	3ad2ant3 1004	. . . . . . . . . . . . . . . . . . 19 ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr inr $/\$ inr ⊔
83	82	impcom 124	. . . . . . . . . . . . . . . . . 18 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr inr $/\$ inr ⊔
84	83	com12 30	. . . . . . . . . . . . . . . . 17 inr $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ inr ⊔
85	84	3ad2ant3 1004	. . . . . . . . . . . . . . . 16 ⊔ $/\$ inl $/\$ inr $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ inr ⊔
86	85	impcom 124	. . . . . . . . . . . . . . 15 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr $/\$ inr ⊔
87	86	com12 30	. . . . . . . . . . . . . 14 $/\$ inr $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
88	87	rexlimiva 2542	. . . . . . . . . . . . 13 inr $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
89	56, 88	jaoi 705	. . . . . . . . . . . 12 inl $\/$ inr $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
90		djur 6947	. . . . . . . . . . . . 13 ⊔ inl $\/$ inr
91	90	biimpi 119	. . . . . . . . . . . 12 ⊔ inl $\/$ inr
92	89, 91	syl11 31	. . . . . . . . . . 11 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔ ⊔
93	92	ralrimiv 2502	. . . . . . . . . 10 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔ ⊔
94		ffn 5267	. . . . . . . . . . . . 13 ⊔ ⊔ ⊔ ⊔
95	94	3ad2ant1 1002	. . . . . . . . . . . 12 ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr ⊔ ⊔
96	95	adantl 275	. . . . . . . . . . 11 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr ⊔ ⊔
97		ffn 5267	. . . . . . . . . . . 12 ⊔ ⊔
98	97	3ad2ant1 1002	. . . . . . . . . . 11 ⊔ $/\$ inl $/\$ inr ⊔
99		eqfnfv 5511	. . . . . . . . . . 11 ⊔ ⊔ $/\$ ⊔ ⊔ ⊔ ⊔
100	96, 98, 99	syl2an 287	. . . . . . . . . 10 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔ ⊔ ⊔
101	93, 100	mpbird 166	. . . . . . . . 9 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
102	101	ex 114	. . . . . . . 8 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr ⊔ $/\$ inl $/\$ inr ⊔
103	102	ralrimivw 2504	. . . . . . 7 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr ⊔ $/\$ inl $/\$ inr ⊔
104	24, 103	jca 304	. . . . . 6 $/\$ ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
105	104	ex 114	. . . . 5 ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
106	21, 22, 23, 105	mp3and 1318	. . . 4 ⊔ ⊔ $/\$ ⊔ inl $/\$ ⊔ inr $/\$ ⊔ $/\$ inl $/\$ inr ⊔
107	6, 17, 106	rspcedvd 2790	. . 3 ⊔ $/\$ inl $/\$ inr $/\$ ⊔ $/\$ inl $/\$ inr
108		feq1 5250	. . . . 5 ⊔ ⊔
109		coeq1 4691	. . . . . 6 inl inl
110	109	eqeq1d 2146	. . . . 5 inl inl
111		coeq1 4691	. . . . . 6 inr inr
112	111	eqeq1d 2146	. . . . 5 inr inr
113	108, 110, 112	3anbi123d 1290	. . . 4 ⊔ $/\$ inl $/\$ inr ⊔ $/\$ inl $/\$ inr
114	113	reu8 2875	. . 3 ⊔ $/\$ inl $/\$ inr ⊔ $/\$ inl $/\$ inr $/\$ ⊔ $/\$ inl $/\$ inr
115	107, 114	sylibr 133	. 2 ⊔ $/\$ inl $/\$ inr
116		reuv 2700	. 2 ⊔ $/\$ inl $/\$ inr ⊔ $/\$ inl $/\$ inr
117	115, 116	sylib 121	1 ⊔ $/\$ inl $/\$ inr

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 697 $/\$ w3a 962

wceq 1331

wcel 1480

weu 1997

wral 2414

wrex 2415

wreu 2416

cvv 2681

c0 3358

cif 3469

cmpt 3984

cres 4536

ccom 4538

wfn 5113

wf 5114

wf1 5115

cfv 5118

c1st 6029

c2nd 6030 ⊔ cdju 6915 inlcinl 6923 inrcinr 6924

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-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-coll 4038 ax-sep 4041 ax-nul 4049 ax-pow 4093 ax-pr 4126 ax-un 4350

This theorem depends on definitions: df-bi 116 df-dc 820 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-eu 2000 df-mo 2001 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ne 2307 df-ral 2419 df-rex 2420 df-reu 2421 df-rab 2423 df-v 2683 df-sbc 2905 df-csb 2999 df-dif 3068 df-un 3070 df-in 3072 df-ss 3079 df-nul 3359 df-if 3470 df-pw 3507 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-iun 3810 df-br 3925 df-opab 3985 df-mpt 3986 df-tr 4022 df-id 4210 df-iord 4283 df-on 4285 df-suc 4288 df-xp 4540 df-rel 4541 df-cnv 4542 df-co 4543 df-dm 4544 df-rn 4545 df-res 4546 df-ima 4547 df-iota 5083 df-fun 5120 df-fn 5121 df-f 5122 df-f1 5123 df-fo 5124 df-f1o 5125 df-fv 5126 df-1st 6031 df-2nd 6032 df-1o 6306 df-dju 6916 df-inl 6925 df-inr 6926

This theorem is referenced by: (None)

W3C validator