dfpo2 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dfpo2		Structured version Unicode version

Theorem dfpo2 29428

Description: Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.)

**Assertion**
Ref	Expression
dfpo2	$/\$

Proof of Theorem dfpo2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		po0 4804	. . . 4
2		res0 5266	. . . . . . 7
3	2	ineq2i 3683	. . . . . 6
4		in0 3810	. . . . . 6
5	3, 4	eqtri 2483	. . . . 5
6		xp0 5410	. . . . . . . . . 10
7	6	ineq2i 3683	. . . . . . . . 9
8	7, 4	eqtri 2483	. . . . . . . 8
9	8	coeq2i 5152	. . . . . . 7
10		co02 5504	. . . . . . 7
11	9, 10	eqtri 2483	. . . . . 6
12		0ss 3813	. . . . . 6
13	11, 12	eqsstri 3519	. . . . 5
14	5, 13	pm3.2i 453	. . . 4 $/\$
15	1, 14	2th 239	. . 3 $/\$
16		poeq2 4793	. . . 4
17		reseq2 5257	. . . . . . 7
18	17	ineq2d 3686	. . . . . 6
19	18	eqeq1d 2456	. . . . 5
20		xpeq2 5003	. . . . . . . 8
21	20	ineq2d 3686	. . . . . . 7
22	21	coeq2d 5154	. . . . . 6
23	22	sseq1d 3516	. . . . 5
24	19, 23	anbi12d 708	. . . 4 $/\$ $/\$
25	16, 24	bibi12d 319	. . 3 $/\$ $/\$
26	15, 25	mpbiri 233	. 2 $/\$
27		r19.28zv 3912	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28	27	ralbidv 2893	. . . . . 6 $/\$ $/\$ $/\$ $/\$
29		r19.28zv 3912	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	28, 29	bitrd 253	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	30	ralbidv 2893	. . . 4 $/\$ $/\$ $/\$ $/\$
32		r19.26 2981	. . . 4 $/\$ $/\$ $/\$ $/\$
33	31, 32	syl6bb 261	. . 3 $/\$ $/\$ $/\$ $/\$
34		df-po 4789	. . 3 $/\$ $/\$
35		disj 3855	. . . . 5
36		df-ral 2809	. . . . 5
37		opex 4701	. . . . . . . . . 10
38		eleq1 2526	. . . . . . . . . . . 12
39		df-br 4440	. . . . . . . . . . . 12
40	38, 39	syl6bbr 263	. . . . . . . . . . 11
41		eleq1 2526	. . . . . . . . . . . . 13
42		vex 3109	. . . . . . . . . . . . . . . 16
43		ididg 5145	. . . . . . . . . . . . . . . 16
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15
45	42	brres 5268	. . . . . . . . . . . . . . 15 $/\$
46	44, 45	mpbiran 916	. . . . . . . . . . . . . 14
47		df-br 4440	. . . . . . . . . . . . . 14
48	46, 47	bitr3i 251	. . . . . . . . . . . . 13
49	41, 48	syl6bbr 263	. . . . . . . . . . . 12
50	49	notbid 292	. . . . . . . . . . 11
51	40, 50	imbi12d 318	. . . . . . . . . 10
52	37, 51	spcv 3197	. . . . . . . . 9
53	52	con2d 115	. . . . . . . 8
54	53	alrimiv 1724	. . . . . . 7
55		relres 5289	. . . . . . . . . . . 12
56		elrel 5093	. . . . . . . . . . . 12 $/\$
57	55, 56	mpan 668	. . . . . . . . . . 11
58	57	ancri 550	. . . . . . . . . 10 $/\$
59		eleq1 2526	. . . . . . . . . . . . . . . 16
60		breq12 4444	. . . . . . . . . . . . . . . . . 18 $/\$
61	60	anidms 643	. . . . . . . . . . . . . . . . 17
62	61	notbid 292	. . . . . . . . . . . . . . . 16
63	59, 62	imbi12d 318	. . . . . . . . . . . . . . 15
64	63	spv 2016	. . . . . . . . . . . . . 14
65		breq2 4443	. . . . . . . . . . . . . . . . . 18
66	65	notbid 292	. . . . . . . . . . . . . . . . 17
67	66	imbi2d 314	. . . . . . . . . . . . . . . 16
68	67	biimpcd 224	. . . . . . . . . . . . . . 15
69	68	impd 429	. . . . . . . . . . . . . 14 $/\$
70	64, 69	syl 16	. . . . . . . . . . . . 13 $/\$
71		eleq1 2526	. . . . . . . . . . . . . . 15
72		vex 3109	. . . . . . . . . . . . . . . . 17
73	72	brres 5268	. . . . . . . . . . . . . . . 16 $/\$
74		df-br 4440	. . . . . . . . . . . . . . . 16
75	72	ideq 5144	. . . . . . . . . . . . . . . . 17
76	75	anbi1i 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	73, 74, 76	3bitr3ri 276	. . . . . . . . . . . . . . 15 $/\$
78	71, 77	syl6bbr 263	. . . . . . . . . . . . . 14 $/\$
79		eleq1 2526	. . . . . . . . . . . . . . . 16
80		df-br 4440	. . . . . . . . . . . . . . . 16
81	79, 80	syl6bbr 263	. . . . . . . . . . . . . . 15
82	81	notbid 292	. . . . . . . . . . . . . 14
83	78, 82	imbi12d 318	. . . . . . . . . . . . 13 $/\$
84	70, 83	syl5ibrcom 222	. . . . . . . . . . . 12
85	84	exlimdvv 1730	. . . . . . . . . . 11
86	85	impd 429	. . . . . . . . . 10 $/\$
87	58, 86	syl5 32	. . . . . . . . 9
88	87	con2d 115	. . . . . . . 8
89	88	alrimiv 1724	. . . . . . 7
90	54, 89	impbii 188	. . . . . 6
91		df-ral 2809	. . . . . 6
92	90, 91	bitr4i 252	. . . . 5
93	35, 36, 92	3bitri 271	. . . 4
94		ralcom 3015	. . . . . . 7 $/\$ $/\$
95		r19.23v 2934	. . . . . . . 8 $/\$ $/\$
96	95	ralbii 2885	. . . . . . 7 $/\$ $/\$
97	94, 96	bitri 249	. . . . . 6 $/\$ $/\$
98	97	ralbii 2885	. . . . 5 $/\$ $/\$
99		brin 4488	. . . . . . . . . . . 12 $/\$
100		brin 4488	. . . . . . . . . . . 12 $/\$
101	99, 100	anbi12i 695	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
102		an4 822	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		ancom 448	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		ancom 448	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	anbi1i 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		brxp 5019	. . . . . . . . . . . . . . 15 $/\$
107		brxp 5019	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	anbi12i 695	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109		anandi 826	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 108, 109	3bitr4i 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
111	110	anbi1i 693	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 103, 111	3bitri 271	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		anass 647	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	101, 112, 113	3bitri 271	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
115	114	exbii 1672	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
116	42, 72	brco 5162	. . . . . . . . . 10 $/\$
117		df-br 4440	. . . . . . . . . 10
118	116, 117	bitr3i 251	. . . . . . . . 9 $/\$
119		df-rex 2810	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120		r19.42v 3009	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	119, 120	bitr3i 251	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 118, 121	3bitr3ri 276	. . . . . . . 8 $/\$ $/\$ $/\$
123		df-br 4440	. . . . . . . 8
124	122, 123	imbi12i 324	. . . . . . 7 $/\$ $/\$ $/\$
125	124	2albii 1646	. . . . . 6 $/\$ $/\$ $/\$
126		r2al 2832	. . . . . . 7 $/\$ $/\$ $/\$
127		impexp 444	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	2albii 1646	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
129	126, 128	bitr4i 252	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130		relco 5488	. . . . . . 7
131		ssrel 5079	. . . . . . 7
132	130, 131	ax-mp 5	. . . . . 6
133	125, 129, 132	3bitr4i 277	. . . . 5 $/\$
134	98, 133	bitr2i 250	. . . 4 $/\$
135	93, 134	anbi12i 695	. . 3 $/\$ $/\$ $/\$
136	33, 34, 135	3bitr4g 288	. 2 $/\$
137	26, 136	pm2.61ine 2767	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367

wal 1396

wceq 1398

wex 1617

wcel 1823

wne 2649

wral 2804

wrex 2805

cvv 3106

cin 3460

wss 3461

c0 3783

cop 4022 class class class wbr 4439

cid 4779

wpo 4787

cxp 4986

cres 4990

ccom 4992

wrel 4993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pr 4676

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-rab 2813 df-v 3108 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3784 df-if 3930 df-sn 4017 df-pr 4019 df-op 4023 df-br 4440 df-opab 4498 df-id 4784 df-po 4789 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-res 5000

This theorem is referenced by: (None)

W3C validator