dfpo2 - Mathbox for Scott Fenton

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

Theorem dfpo2 25326

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 4478	. . . 4
2		res0 5109	. . . . . . 7
3	2	ineq2i 3499	. . . . . 6
4		in0 3613	. . . . . 6
5	3, 4	eqtri 2424	. . . . 5
6		xp0 5250	. . . . . . . . . 10
7	6	ineq2i 3499	. . . . . . . . 9
8	7, 4	eqtri 2424	. . . . . . . 8
9	8	coeq2i 4992	. . . . . . 7
10		co02 5342	. . . . . . 7
11	9, 10	eqtri 2424	. . . . . 6
12		0ss 3616	. . . . . 6
13	11, 12	eqsstri 3338	. . . . 5
14	5, 13	pm3.2i 442	. . . 4 $/\$
15	1, 14	2th 231	. . 3 $/\$
16		poeq2 4467	. . . 4
17		reseq2 5100	. . . . . . 7
18	17	ineq2d 3502	. . . . . 6
19	18	eqeq1d 2412	. . . . 5
20		xpeq2 4852	. . . . . . . 8
21	20	ineq2d 3502	. . . . . . 7
22	21	coeq2d 4994	. . . . . 6
23	22	sseq1d 3335	. . . . 5
24	19, 23	anbi12d 692	. . . 4 $/\$ $/\$
25	16, 24	bibi12d 313	. . 3 $/\$ $/\$
26	15, 25	mpbiri 225	. 2 $/\$
27		r19.28zv 3683	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28	27	ralbidv 2686	. . . . . 6 $/\$ $/\$ $/\$ $/\$
29		r19.28zv 3683	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	28, 29	bitrd 245	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	30	ralbidv 2686	. . . 4 $/\$ $/\$ $/\$ $/\$
32		r19.26 2798	. . . 4 $/\$ $/\$ $/\$ $/\$
33	31, 32	syl6bb 253	. . 3 $/\$ $/\$ $/\$ $/\$
34		df-po 4463	. . 3 $/\$ $/\$
35		disj 3628	. . . . 5
36		df-ral 2671	. . . . 5
37		opex 4387	. . . . . . . . . 10
38		eleq1 2464	. . . . . . . . . . . 12
39		df-br 4173	. . . . . . . . . . . 12
40	38, 39	syl6bbr 255	. . . . . . . . . . 11
41		eleq1 2464	. . . . . . . . . . . . 13
42		vex 2919	. . . . . . . . . . . . . . . 16
43		ididg 4985	. . . . . . . . . . . . . . . 16
44	42, 43	ax-mp 8	. . . . . . . . . . . . . . 15
45	42	brres 5111	. . . . . . . . . . . . . . 15 $/\$
46	44, 45	mpbiran 885	. . . . . . . . . . . . . 14
47		df-br 4173	. . . . . . . . . . . . . 14
48	46, 47	bitr3i 243	. . . . . . . . . . . . 13
49	41, 48	syl6bbr 255	. . . . . . . . . . . 12
50	49	notbid 286	. . . . . . . . . . 11
51	40, 50	imbi12d 312	. . . . . . . . . 10
52	37, 51	spcv 3002	. . . . . . . . 9
53	52	con2d 109	. . . . . . . 8
54	53	alrimiv 1638	. . . . . . 7
55		relres 5133	. . . . . . . . . . . 12
56		elrel 4937	. . . . . . . . . . . 12 $/\$
57	55, 56	mpan 652	. . . . . . . . . . 11
58	57	ancri 536	. . . . . . . . . 10 $/\$
59		eleq1 2464	. . . . . . . . . . . . . . . 16
60		breq12 4177	. . . . . . . . . . . . . . . . . 18 $/\$
61	60	anidms 627	. . . . . . . . . . . . . . . . 17
62	61	notbid 286	. . . . . . . . . . . . . . . 16
63	59, 62	imbi12d 312	. . . . . . . . . . . . . . 15
64	63	spv 1963	. . . . . . . . . . . . . 14
65		breq2 4176	. . . . . . . . . . . . . . . . . 18
66	65	notbid 286	. . . . . . . . . . . . . . . . 17
67	66	imbi2d 308	. . . . . . . . . . . . . . . 16
68	67	biimpcd 216	. . . . . . . . . . . . . . 15
69	68	imp3a 421	. . . . . . . . . . . . . 14 $/\$
70	64, 69	syl 16	. . . . . . . . . . . . 13 $/\$
71		eleq1 2464	. . . . . . . . . . . . . . 15
72		vex 2919	. . . . . . . . . . . . . . . . 17
73	72	brres 5111	. . . . . . . . . . . . . . . 16 $/\$
74		df-br 4173	. . . . . . . . . . . . . . . 16
75	72	ideq 4984	. . . . . . . . . . . . . . . . 17
76	75	anbi1i 677	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	73, 74, 76	3bitr3ri 268	. . . . . . . . . . . . . . 15 $/\$
78	71, 77	syl6bbr 255	. . . . . . . . . . . . . 14 $/\$
79		eleq1 2464	. . . . . . . . . . . . . . . 16
80		df-br 4173	. . . . . . . . . . . . . . . 16
81	79, 80	syl6bbr 255	. . . . . . . . . . . . . . 15
82	81	notbid 286	. . . . . . . . . . . . . 14
83	78, 82	imbi12d 312	. . . . . . . . . . . . 13 $/\$
84	70, 83	syl5ibrcom 214	. . . . . . . . . . . 12
85	84	exlimdvv 1644	. . . . . . . . . . 11
86	85	imp3a 421	. . . . . . . . . 10 $/\$
87	58, 86	syl5 30	. . . . . . . . 9
88	87	con2d 109	. . . . . . . 8
89	88	alrimiv 1638	. . . . . . 7
90	54, 89	impbii 181	. . . . . 6
91		df-ral 2671	. . . . . 6
92	90, 91	bitr4i 244	. . . . 5
93	35, 36, 92	3bitri 263	. . . 4
94		ralcom 2828	. . . . . . 7 $/\$ $/\$
95		r19.23v 2782	. . . . . . . 8 $/\$ $/\$
96	95	ralbii 2690	. . . . . . 7 $/\$ $/\$
97	94, 96	bitri 241	. . . . . 6 $/\$ $/\$
98	97	ralbii 2690	. . . . 5 $/\$ $/\$
99		brin 4219	. . . . . . . . . . . 12 $/\$
100		brin 4219	. . . . . . . . . . . 12 $/\$
101	99, 100	anbi12i 679	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
102		an4 798	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		ancom 438	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		ancom 438	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	anbi1i 677	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		brxp 4868	. . . . . . . . . . . . . . 15 $/\$
107		brxp 4868	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	anbi12i 679	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109		anandi 802	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 108, 109	3bitr4i 269	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
111	110	anbi1i 677	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 103, 111	3bitri 263	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		anass 631	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	101, 112, 113	3bitri 263	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
115	114	exbii 1589	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
116	42, 72	brco 5002	. . . . . . . . . 10 $/\$
117		df-br 4173	. . . . . . . . . 10
118	116, 117	bitr3i 243	. . . . . . . . 9 $/\$
119		df-rex 2672	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120		r19.42v 2822	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	119, 120	bitr3i 243	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 118, 121	3bitr3ri 268	. . . . . . . 8 $/\$ $/\$ $/\$
123		df-br 4173	. . . . . . . 8
124	122, 123	imbi12i 317	. . . . . . 7 $/\$ $/\$ $/\$
125	124	2albii 1573	. . . . . 6 $/\$ $/\$ $/\$
126		r2al 2703	. . . . . . 7 $/\$ $/\$ $/\$
127		impexp 434	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	2albii 1573	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
129	126, 128	bitr4i 244	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130		relco 5327	. . . . . . 7
131		ssrel 4923	. . . . . . 7
132	130, 131	ax-mp 8	. . . . . 6
133	125, 129, 132	3bitr4i 269	. . . . 5 $/\$
134	98, 133	bitr2i 242	. . . 4 $/\$
135	93, 134	anbi12i 679	. . 3 $/\$ $/\$ $/\$
136	33, 34, 135	3bitr4g 280	. 2 $/\$
137	26, 136	pm2.61ine 2643	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359

wal 1546

wex 1547

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cvv 2916

cin 3279

wss 3280

c0 3588

cop 3777 class class class wbr 4172

cid 4453

wpo 4461

cxp 4835

cres 4839

ccom 4841

wrel 4842

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pr 4363

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-rab 2675 df-v 2918 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-sn 3780 df-pr 3781 df-op 3783 df-br 4173 df-opab 4227 df-id 4458 df-po 4463 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-res 4849

W3C validator