disjunsn - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > disjunsn		Structured version Visualization version Unicode version

Theorem disjunsn 29407

Description: Append an element to a disjoint collection. Similar to ralunsn 4422, gsumunsn 18359, etc. (Contributed by Thierry Arnoux, 28-Mar-2018.)

**Hypothesis**
Ref	Expression
disjunsn.s

**Assertion**
Ref	Expression
disjunsn	$/\$ Disj Disj $/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem disjunsn Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		disjors 4635	. . . . . 6 Disj $\/$
2		eqeq1 2626	. . . . . . . . 9
3		csbeq1 3536	. . . . . . . . . . 11
4	3	ineq1d 3813	. . . . . . . . . 10
5	4	eqeq1d 2624	. . . . . . . . 9
6	2, 5	orbi12d 746	. . . . . . . 8 $\/$ $\/$
7	6	ralbidv 2986	. . . . . . 7 $\/$ $\/$
8	7	ralunsn 4422	. . . . . 6 $\/$ $\/$ $/\$ $\/$
9	1, 8	syl5bb 272	. . . . 5 Disj $\/$ $/\$ $\/$
10		eqeq2 2633	. . . . . . . . 9
11		csbeq1 3536	. . . . . . . . . . 11
12	11	ineq2d 3814	. . . . . . . . . 10
13	12	eqeq1d 2624	. . . . . . . . 9
14	10, 13	orbi12d 746	. . . . . . . 8 $\/$ $\/$
15	14	ralunsn 4422	. . . . . . 7 $\/$ $\/$ $/\$ $\/$
16	15	ralbidv 2986	. . . . . 6 $\/$ $\/$ $/\$ $\/$
17		eqeq2 2633	. . . . . . . . 9
18	11	ineq2d 3814	. . . . . . . . . 10
19	18	eqeq1d 2624	. . . . . . . . 9
20	17, 19	orbi12d 746	. . . . . . . 8 $\/$ $\/$
21	20	ralunsn 4422	. . . . . . 7 $\/$ $\/$ $/\$ $\/$
22		eqid 2622	. . . . . . . . 9
23	22	orci 405	. . . . . . . 8 $\/$
24	23	biantru 526	. . . . . . 7 $\/$ $\/$ $/\$ $\/$
25	21, 24	syl6bbr 278	. . . . . 6 $\/$ $\/$
26	16, 25	anbi12d 747	. . . . 5 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
27	9, 26	bitrd 268	. . . 4 Disj $\/$ $/\$ $\/$ $/\$ $\/$
28		r19.26 3064	. . . . . 6 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
29		disjors 4635	. . . . . . 7 Disj $\/$
30	29	anbi1i 731	. . . . . 6 Disj $/\$ $\/$ $\/$ $/\$ $\/$
31	28, 30	bitr4i 267	. . . . 5 $\/$ $/\$ $\/$ Disj $/\$ $\/$
32	31	anbi1i 731	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$ Disj $/\$ $\/$ $/\$ $\/$
33	27, 32	syl6bb 276	. . 3 Disj Disj $/\$ $\/$ $/\$ $\/$
34	33	adantr 481	. 2 $/\$ Disj Disj $/\$ $\/$ $/\$ $\/$
35		orcom 402	. . . . . . . . 9 $\/$ $\/$
36	35	ralbii 2980	. . . . . . . 8 $\/$ $\/$
37		r19.30 3082	. . . . . . . . 9 $\/$ $\/$
38		risset 3062	. . . . . . . . . . . 12
39		biorf 420	. . . . . . . . . . . 12 $\/$
40	38, 39	sylnbi 320	. . . . . . . . . . 11 $\/$
41	40	adantl 482	. . . . . . . . . 10 $/\$ $\/$
42		orcom 402	. . . . . . . . . 10 $\/$ $\/$
43	41, 42	syl6bb 276	. . . . . . . . 9 $/\$ $\/$
44	37, 43	syl5ibr 236	. . . . . . . 8 $/\$ $\/$
45	36, 44	syl5bir 233	. . . . . . 7 $/\$ $\/$
46		olc 399	. . . . . . . 8 $\/$
47	46	ralimi 2952	. . . . . . 7 $\/$
48	45, 47	impbid1 215	. . . . . 6 $/\$ $\/$
49		nfv 1843	. . . . . . . . . 10
50		nfcsb1v 3549	. . . . . . . . . . . 12
51		nfcv 2764	. . . . . . . . . . . 12
52	50, 51	nfin 3820	. . . . . . . . . . 11
53	52	nfeq1 2778	. . . . . . . . . 10
54		csbeq1a 3542	. . . . . . . . . . . 12
55	54	ineq1d 3813	. . . . . . . . . . 11
56	55	eqeq1d 2624	. . . . . . . . . 10
57	49, 53, 56	cbvral 3167	. . . . . . . . 9
58	57	a1i 11	. . . . . . . 8
59		ss0b 3973	. . . . . . . . . . 11
60		iunss 4561	. . . . . . . . . . 11
61		iunin1 4585	. . . . . . . . . . . 12
62	61	eqeq1i 2627	. . . . . . . . . . 11
63	59, 60, 62	3bitr3ri 291	. . . . . . . . . 10
64		ss0b 3973	. . . . . . . . . . 11
65	64	ralbii 2980	. . . . . . . . . 10
66	63, 65	bitri 264	. . . . . . . . 9
67	66	a1i 11	. . . . . . . 8
68		nfcvd 2765	. . . . . . . . . . . 12
69		disjunsn.s	. . . . . . . . . . . 12
70	68, 69	csbiegf 3557	. . . . . . . . . . 11
71	70	ineq2d 3814	. . . . . . . . . 10
72	71	eqeq1d 2624	. . . . . . . . 9
73	72	ralbidv 2986	. . . . . . . 8
74	58, 67, 73	3bitr4d 300	. . . . . . 7
75	74	adantr 481	. . . . . 6 $/\$
76	48, 75	bitr4d 271	. . . . 5 $/\$ $\/$
77	76	anbi2d 740	. . . 4 $/\$ Disj $/\$ $\/$ Disj $/\$
78		orcom 402	. . . . . . . 8 $\/$ $\/$
79	78	ralbii 2980	. . . . . . 7 $\/$ $\/$
80		r19.30 3082	. . . . . . . 8 $\/$ $\/$
81		clel5 3343	. . . . . . . . . . 11
82		biorf 420	. . . . . . . . . . 11 $\/$
83	81, 82	sylnbi 320	. . . . . . . . . 10 $\/$
84	83	adantl 482	. . . . . . . . 9 $/\$ $\/$
85		orcom 402	. . . . . . . . 9 $\/$ $\/$
86	84, 85	syl6bb 276	. . . . . . . 8 $/\$ $\/$
87	80, 86	syl5ibr 236	. . . . . . 7 $/\$ $\/$
88	79, 87	syl5bir 233	. . . . . 6 $/\$ $\/$
89		olc 399	. . . . . . 7 $\/$
90	89	ralimi 2952	. . . . . 6 $\/$
91	88, 90	impbid1 215	. . . . 5 $/\$ $\/$
92		nfv 1843	. . . . . . . . . 10
93		nfcsb1v 3549	. . . . . . . . . . . 12
94	93, 51	nfin 3820	. . . . . . . . . . 11
95	94	nfeq1 2778	. . . . . . . . . 10
96		csbeq1a 3542	. . . . . . . . . . . 12
97	96	ineq1d 3813	. . . . . . . . . . 11
98	97	eqeq1d 2624	. . . . . . . . . 10
99	92, 95, 98	cbvral 3167	. . . . . . . . 9
100	99	a1i 11	. . . . . . . 8
101		incom 3805	. . . . . . . . . 10
102	101	eqeq1i 2627	. . . . . . . . 9
103	102	ralbii 2980	. . . . . . . 8
104	100, 103	syl6bb 276	. . . . . . 7
105	70	ineq1d 3813	. . . . . . . . 9
106	105	eqeq1d 2624	. . . . . . . 8
107	106	ralbidv 2986	. . . . . . 7
108	104, 67, 107	3bitr4d 300	. . . . . 6
109	108	adantr 481	. . . . 5 $/\$
110	91, 109	bitr4d 271	. . . 4 $/\$ $\/$
111	77, 110	anbi12d 747	. . 3 $/\$ Disj $/\$ $\/$ $/\$ $\/$ Disj $/\$ $/\$
112		anass 681	. . . 4 Disj $/\$ $/\$ Disj $/\$ $/\$
113		anidm 676	. . . . 5 $/\$
114	113	anbi2i 730	. . . 4 Disj $/\$ $/\$ Disj $/\$
115	112, 114	bitri 264	. . 3 Disj $/\$ $/\$ Disj $/\$
116	111, 115	syl6bb 276	. 2 $/\$ Disj $/\$ $\/$ $/\$ $\/$ Disj $/\$
117	34, 116	bitrd 268	1 $/\$ Disj Disj $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wral 2912

wrex 2913

csb 3533

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

ciun 4520 Disj wdisj 4620

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-sn 4178 df-iun 4522 df-disj 4621

This theorem is referenced by: disjun0 29408 disjiunel 29409

W3C validator