dfpo2 - Mathbox for Scott Fenton

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

Theorem dfpo2 31645

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 5050	. . . 4
2		res0 5400	. . . . . . 7
3	2	ineq2i 3811	. . . . . 6
4		in0 3968	. . . . . 6
5	3, 4	eqtri 2644	. . . . 5
6		xp0 5552	. . . . . . . . . 10
7	6	ineq2i 3811	. . . . . . . . 9
8	7, 4	eqtri 2644	. . . . . . . 8
9	8	coeq2i 5282	. . . . . . 7
10		co02 5649	. . . . . . 7
11	9, 10	eqtri 2644	. . . . . 6
12		0ss 3972	. . . . . 6
13	11, 12	eqsstri 3635	. . . . 5
14	5, 13	pm3.2i 471	. . . 4 $/\$
15	1, 14	2th 254	. . 3 $/\$
16		poeq2 5039	. . . 4
17		reseq2 5391	. . . . . . 7
18	17	ineq2d 3814	. . . . . 6
19	18	eqeq1d 2624	. . . . 5
20		xpeq2 5129	. . . . . . . 8
21	20	ineq2d 3814	. . . . . . 7
22	21	coeq2d 5284	. . . . . 6
23	22	sseq1d 3632	. . . . 5
24	19, 23	anbi12d 747	. . . 4 $/\$ $/\$
25	16, 24	bibi12d 335	. . 3 $/\$ $/\$
26	15, 25	mpbiri 248	. 2 $/\$
27		r19.28zv 4066	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28	27	ralbidv 2986	. . . . . 6 $/\$ $/\$ $/\$ $/\$
29		r19.28zv 4066	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	28, 29	bitrd 268	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	30	ralbidv 2986	. . . 4 $/\$ $/\$ $/\$ $/\$
32		r19.26 3064	. . . 4 $/\$ $/\$ $/\$ $/\$
33	31, 32	syl6bb 276	. . 3 $/\$ $/\$ $/\$ $/\$
34		df-po 5035	. . 3 $/\$ $/\$
35		disj 4017	. . . . 5
36		df-ral 2917	. . . . 5
37		opex 4932	. . . . . . . . . 10
38		eleq1 2689	. . . . . . . . . . . 12
39		df-br 4654	. . . . . . . . . . . 12
40	38, 39	syl6bbr 278	. . . . . . . . . . 11
41		eleq1 2689	. . . . . . . . . . . . 13
42		vex 3203	. . . . . . . . . . . . . . . 16
43		ididg 5275	. . . . . . . . . . . . . . . 16
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15
45	42	brres 5402	. . . . . . . . . . . . . . 15 $/\$
46	44, 45	mpbiran 953	. . . . . . . . . . . . . 14
47		df-br 4654	. . . . . . . . . . . . . 14
48	46, 47	bitr3i 266	. . . . . . . . . . . . 13
49	41, 48	syl6bbr 278	. . . . . . . . . . . 12
50	49	notbid 308	. . . . . . . . . . 11
51	40, 50	imbi12d 334	. . . . . . . . . 10
52	37, 51	spcv 3299	. . . . . . . . 9
53	52	con2d 129	. . . . . . . 8
54	53	alrimiv 1855	. . . . . . 7
55		relres 5426	. . . . . . . . . . . 12
56		elrel 5222	. . . . . . . . . . . 12 $/\$
57	55, 56	mpan 706	. . . . . . . . . . 11
58	57	ancri 575	. . . . . . . . . 10 $/\$
59		eleq1 2689	. . . . . . . . . . . . . . . 16
60		breq12 4658	. . . . . . . . . . . . . . . . . 18 $/\$
61	60	anidms 677	. . . . . . . . . . . . . . . . 17
62	61	notbid 308	. . . . . . . . . . . . . . . 16
63	59, 62	imbi12d 334	. . . . . . . . . . . . . . 15
64	63	spv 2260	. . . . . . . . . . . . . 14
65		breq2 4657	. . . . . . . . . . . . . . . . . 18
66	65	notbid 308	. . . . . . . . . . . . . . . . 17
67	66	imbi2d 330	. . . . . . . . . . . . . . . 16
68	67	biimpcd 239	. . . . . . . . . . . . . . 15
69	68	impd 447	. . . . . . . . . . . . . 14 $/\$
70	64, 69	syl 17	. . . . . . . . . . . . 13 $/\$
71		eleq1 2689	. . . . . . . . . . . . . . 15
72		vex 3203	. . . . . . . . . . . . . . . . 17
73	72	brres 5402	. . . . . . . . . . . . . . . 16 $/\$
74		df-br 4654	. . . . . . . . . . . . . . . 16
75	72	ideq 5274	. . . . . . . . . . . . . . . . 17
76	75	anbi1i 731	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	73, 74, 76	3bitr3ri 291	. . . . . . . . . . . . . . 15 $/\$
78	71, 77	syl6bbr 278	. . . . . . . . . . . . . 14 $/\$
79		eleq1 2689	. . . . . . . . . . . . . . . 16
80		df-br 4654	. . . . . . . . . . . . . . . 16
81	79, 80	syl6bbr 278	. . . . . . . . . . . . . . 15
82	81	notbid 308	. . . . . . . . . . . . . 14
83	78, 82	imbi12d 334	. . . . . . . . . . . . 13 $/\$
84	70, 83	syl5ibrcom 237	. . . . . . . . . . . 12
85	84	exlimdvv 1862	. . . . . . . . . . 11
86	85	impd 447	. . . . . . . . . 10 $/\$
87	58, 86	syl5 34	. . . . . . . . 9
88	87	con2d 129	. . . . . . . 8
89	88	alrimiv 1855	. . . . . . 7
90	54, 89	impbii 199	. . . . . 6
91		df-ral 2917	. . . . . 6
92	90, 91	bitr4i 267	. . . . 5
93	35, 36, 92	3bitri 286	. . . 4
94		ralcom 3098	. . . . . . 7 $/\$ $/\$
95		r19.23v 3023	. . . . . . . 8 $/\$ $/\$
96	95	ralbii 2980	. . . . . . 7 $/\$ $/\$
97	94, 96	bitri 264	. . . . . 6 $/\$ $/\$
98	97	ralbii 2980	. . . . 5 $/\$ $/\$
99		brin 4704	. . . . . . . . . . . 12 $/\$
100		brin 4704	. . . . . . . . . . . 12 $/\$
101	99, 100	anbi12i 733	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
102		an4 865	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		ancom 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		ancom 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	anbi1i 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		brxp 5147	. . . . . . . . . . . . . . 15 $/\$
107		brxp 5147	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	anbi12i 733	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109		anandi 871	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 108, 109	3bitr4i 292	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
111	110	anbi1i 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 103, 111	3bitri 286	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		anass 681	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	101, 112, 113	3bitri 286	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
115	114	exbii 1774	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
116	42, 72	brco 5292	. . . . . . . . . 10 $/\$
117		df-br 4654	. . . . . . . . . 10
118	116, 117	bitr3i 266	. . . . . . . . 9 $/\$
119		df-rex 2918	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120		r19.42v 3092	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	119, 120	bitr3i 266	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 118, 121	3bitr3ri 291	. . . . . . . 8 $/\$ $/\$ $/\$
123		df-br 4654	. . . . . . . 8
124	122, 123	imbi12i 340	. . . . . . 7 $/\$ $/\$ $/\$
125	124	2albii 1748	. . . . . 6 $/\$ $/\$ $/\$
126		r2al 2939	. . . . . . 7 $/\$ $/\$ $/\$
127		impexp 462	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	2albii 1748	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
129	126, 128	bitr4i 267	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130		relco 5633	. . . . . . 7
131		ssrel 5207	. . . . . . 7
132	130, 131	ax-mp 5	. . . . . 6
133	125, 129, 132	3bitr4i 292	. . . . 5 $/\$
134	98, 133	bitr2i 265	. . . 4 $/\$
135	93, 134	anbi12i 733	. . 3 $/\$ $/\$ $/\$
136	33, 34, 135	3bitr4g 303	. 2 $/\$
137	26, 136	pm2.61ine 2877	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wal 1481

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200

cin 3573

wss 3574

c0 3915

cop 4183 class class class wbr 4653

cid 5023

wpo 5033

cxp 5112

cres 5116

ccom 5118

wrel 5119

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 ax-sep 4781 ax-nul 4789 ax-pr 4906

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-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-id 5024 df-po 5035 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-res 5126

This theorem is referenced by: (None)

W3C validator