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 28761

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 4815	. . . 4
2		res0 5276	. . . . . . 7
3	2	ineq2i 3697	. . . . . 6
4		in0 3811	. . . . . 6
5	3, 4	eqtri 2496	. . . . 5
6		xp0 5423	. . . . . . . . . 10
7	6	ineq2i 3697	. . . . . . . . 9
8	7, 4	eqtri 2496	. . . . . . . 8
9	8	coeq2i 5161	. . . . . . 7
10		co02 5519	. . . . . . 7
11	9, 10	eqtri 2496	. . . . . 6
12		0ss 3814	. . . . . 6
13	11, 12	eqsstri 3534	. . . . 5
14	5, 13	pm3.2i 455	. . . 4 $/\$
15	1, 14	2th 239	. . 3 $/\$
16		poeq2 4804	. . . 4
17		reseq2 5266	. . . . . . 7
18	17	ineq2d 3700	. . . . . 6
19	18	eqeq1d 2469	. . . . 5
20		xpeq2 5014	. . . . . . . 8
21	20	ineq2d 3700	. . . . . . 7
22	21	coeq2d 5163	. . . . . 6
23	22	sseq1d 3531	. . . . 5
24	19, 23	anbi12d 710	. . . 4 $/\$ $/\$
25	16, 24	bibi12d 321	. . 3 $/\$ $/\$
26	15, 25	mpbiri 233	. 2 $/\$
27		r19.28zv 3923	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28	27	ralbidv 2903	. . . . . 6 $/\$ $/\$ $/\$ $/\$
29		r19.28zv 3923	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	28, 29	bitrd 253	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	30	ralbidv 2903	. . . 4 $/\$ $/\$ $/\$ $/\$
32		r19.26 2989	. . . 4 $/\$ $/\$ $/\$ $/\$
33	31, 32	syl6bb 261	. . 3 $/\$ $/\$ $/\$ $/\$
34		df-po 4800	. . 3 $/\$ $/\$
35		disj 3867	. . . . 5
36		df-ral 2819	. . . . 5
37		opex 4711	. . . . . . . . . 10
38		eleq1 2539	. . . . . . . . . . . 12
39		df-br 4448	. . . . . . . . . . . 12
40	38, 39	syl6bbr 263	. . . . . . . . . . 11
41		eleq1 2539	. . . . . . . . . . . . 13
42		vex 3116	. . . . . . . . . . . . . . . 16
43		ididg 5154	. . . . . . . . . . . . . . . 16
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15
45	42	brres 5278	. . . . . . . . . . . . . . 15 $/\$
46	44, 45	mpbiran 916	. . . . . . . . . . . . . 14
47		df-br 4448	. . . . . . . . . . . . . 14
48	46, 47	bitr3i 251	. . . . . . . . . . . . 13
49	41, 48	syl6bbr 263	. . . . . . . . . . . 12
50	49	notbid 294	. . . . . . . . . . 11
51	40, 50	imbi12d 320	. . . . . . . . . 10
52	37, 51	spcv 3204	. . . . . . . . 9
53	52	con2d 115	. . . . . . . 8
54	53	alrimiv 1695	. . . . . . 7
55		relres 5299	. . . . . . . . . . . 12
56		elrel 5103	. . . . . . . . . . . 12 $/\$
57	55, 56	mpan 670	. . . . . . . . . . 11
58	57	ancri 552	. . . . . . . . . 10 $/\$
59		eleq1 2539	. . . . . . . . . . . . . . . 16
60		breq12 4452	. . . . . . . . . . . . . . . . . 18 $/\$
61	60	anidms 645	. . . . . . . . . . . . . . . . 17
62	61	notbid 294	. . . . . . . . . . . . . . . 16
63	59, 62	imbi12d 320	. . . . . . . . . . . . . . 15
64	63	spv 1980	. . . . . . . . . . . . . 14
65		breq2 4451	. . . . . . . . . . . . . . . . . 18
66	65	notbid 294	. . . . . . . . . . . . . . . . 17
67	66	imbi2d 316	. . . . . . . . . . . . . . . 16
68	67	biimpcd 224	. . . . . . . . . . . . . . 15
69	68	impd 431	. . . . . . . . . . . . . 14 $/\$
70	64, 69	syl 16	. . . . . . . . . . . . 13 $/\$
71		eleq1 2539	. . . . . . . . . . . . . . 15
72		vex 3116	. . . . . . . . . . . . . . . . 17
73	72	brres 5278	. . . . . . . . . . . . . . . 16 $/\$
74		df-br 4448	. . . . . . . . . . . . . . . 16
75	72	ideq 5153	. . . . . . . . . . . . . . . . 17
76	75	anbi1i 695	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	73, 74, 76	3bitr3ri 276	. . . . . . . . . . . . . . 15 $/\$
78	71, 77	syl6bbr 263	. . . . . . . . . . . . . 14 $/\$
79		eleq1 2539	. . . . . . . . . . . . . . . 16
80		df-br 4448	. . . . . . . . . . . . . . . 16
81	79, 80	syl6bbr 263	. . . . . . . . . . . . . . 15
82	81	notbid 294	. . . . . . . . . . . . . 14
83	78, 82	imbi12d 320	. . . . . . . . . . . . 13 $/\$
84	70, 83	syl5ibrcom 222	. . . . . . . . . . . 12
85	84	exlimdvv 1701	. . . . . . . . . . 11
86	85	impd 431	. . . . . . . . . 10 $/\$
87	58, 86	syl5 32	. . . . . . . . 9
88	87	con2d 115	. . . . . . . 8
89	88	alrimiv 1695	. . . . . . 7
90	54, 89	impbii 188	. . . . . 6
91		df-ral 2819	. . . . . 6
92	90, 91	bitr4i 252	. . . . 5
93	35, 36, 92	3bitri 271	. . . 4
94		ralcom 3022	. . . . . . 7 $/\$ $/\$
95		r19.23v 2943	. . . . . . . 8 $/\$ $/\$
96	95	ralbii 2895	. . . . . . 7 $/\$ $/\$
97	94, 96	bitri 249	. . . . . 6 $/\$ $/\$
98	97	ralbii 2895	. . . . 5 $/\$ $/\$
99		brin 4496	. . . . . . . . . . . 12 $/\$
100		brin 4496	. . . . . . . . . . . 12 $/\$
101	99, 100	anbi12i 697	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
102		an4 822	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		ancom 450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		ancom 450	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	anbi1i 695	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		brxp 5029	. . . . . . . . . . . . . . 15 $/\$
107		brxp 5029	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	anbi12i 697	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109		anandi 826	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 108, 109	3bitr4i 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
111	110	anbi1i 695	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 103, 111	3bitri 271	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		anass 649	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	101, 112, 113	3bitri 271	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
115	114	exbii 1644	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
116	42, 72	brco 5171	. . . . . . . . . 10 $/\$
117		df-br 4448	. . . . . . . . . 10
118	116, 117	bitr3i 251	. . . . . . . . 9 $/\$
119		df-rex 2820	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120		r19.42v 3016	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	119, 120	bitr3i 251	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 118, 121	3bitr3ri 276	. . . . . . . 8 $/\$ $/\$ $/\$
123		df-br 4448	. . . . . . . 8
124	122, 123	imbi12i 326	. . . . . . 7 $/\$ $/\$ $/\$
125	124	2albii 1621	. . . . . 6 $/\$ $/\$ $/\$
126		r2al 2842	. . . . . . 7 $/\$ $/\$ $/\$
127		impexp 446	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	2albii 1621	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
129	126, 128	bitr4i 252	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130		relco 5503	. . . . . . 7
131		ssrel 5089	. . . . . . 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 697	. . 3 $/\$ $/\$ $/\$
136	33, 34, 135	3bitr4g 288	. 2 $/\$
137	26, 136	pm2.61ine 2780	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wal 1377

wceq 1379

wex 1596

wcel 1767

wne 2662

wral 2814

wrex 2815

cvv 3113

cin 3475

wss 3476

c0 3785

cop 4033 class class class wbr 4447

cid 4790

wpo 4798

cxp 4997

cres 5001

ccom 5003

wrel 5004

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pr 4686

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-sn 4028 df-pr 4030 df-op 4034 df-br 4448 df-opab 4506 df-id 4795 df-po 4800 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-res 5011

This theorem is referenced by: (None)

W3C validator