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 30443

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 4788	. . . 4
2		res0 5127	. . . . . . 7
3	2	ineq2i 3642	. . . . . 6
4		in0 3771	. . . . . 6
5	3, 4	eqtri 2483	. . . . 5
6		xp0 5273	. . . . . . . . . 10
7	6	ineq2i 3642	. . . . . . . . 9
8	7, 4	eqtri 2483	. . . . . . . 8
9	8	coeq2i 5013	. . . . . . 7
10		co02 5367	. . . . . . 7
11	9, 10	eqtri 2483	. . . . . 6
12		0ss 3774	. . . . . 6
13	11, 12	eqsstri 3473	. . . . 5
14	5, 13	pm3.2i 461	. . . 4 $/\$
15	1, 14	2th 247	. . 3 $/\$
16		poeq2 4777	. . . 4
17		reseq2 5118	. . . . . . 7
18	17	ineq2d 3645	. . . . . 6
19	18	eqeq1d 2463	. . . . 5
20		xpeq2 4867	. . . . . . . 8
21	20	ineq2d 3645	. . . . . . 7
22	21	coeq2d 5015	. . . . . 6
23	22	sseq1d 3470	. . . . 5
24	19, 23	anbi12d 722	. . . 4 $/\$ $/\$
25	16, 24	bibi12d 327	. . 3 $/\$ $/\$
26	15, 25	mpbiri 241	. 2 $/\$
27		r19.28zv 3875	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28	27	ralbidv 2838	. . . . . 6 $/\$ $/\$ $/\$ $/\$
29		r19.28zv 3875	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	28, 29	bitrd 261	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	30	ralbidv 2838	. . . 4 $/\$ $/\$ $/\$ $/\$
32		r19.26 2928	. . . 4 $/\$ $/\$ $/\$ $/\$
33	31, 32	syl6bb 269	. . 3 $/\$ $/\$ $/\$ $/\$
34		df-po 4773	. . 3 $/\$ $/\$
35		disj 3816	. . . . 5
36		df-ral 2753	. . . . 5
37		opex 4677	. . . . . . . . . 10
38		eleq1 2527	. . . . . . . . . . . 12
39		df-br 4416	. . . . . . . . . . . 12
40	38, 39	syl6bbr 271	. . . . . . . . . . 11
41		eleq1 2527	. . . . . . . . . . . . 13
42		vex 3059	. . . . . . . . . . . . . . . 16
43		ididg 5006	. . . . . . . . . . . . . . . 16
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15
45	42	brres 5129	. . . . . . . . . . . . . . 15 $/\$
46	44, 45	mpbiran 934	. . . . . . . . . . . . . 14
47		df-br 4416	. . . . . . . . . . . . . 14
48	46, 47	bitr3i 259	. . . . . . . . . . . . 13
49	41, 48	syl6bbr 271	. . . . . . . . . . . 12
50	49	notbid 300	. . . . . . . . . . 11
51	40, 50	imbi12d 326	. . . . . . . . . 10
52	37, 51	spcv 3151	. . . . . . . . 9
53	52	con2d 120	. . . . . . . 8
54	53	alrimiv 1783	. . . . . . 7
55		relres 5150	. . . . . . . . . . . 12
56		elrel 4955	. . . . . . . . . . . 12 $/\$
57	55, 56	mpan 681	. . . . . . . . . . 11
58	57	ancri 559	. . . . . . . . . 10 $/\$
59		eleq1 2527	. . . . . . . . . . . . . . . 16
60		breq12 4420	. . . . . . . . . . . . . . . . . 18 $/\$
61	60	anidms 655	. . . . . . . . . . . . . . . . 17
62	61	notbid 300	. . . . . . . . . . . . . . . 16
63	59, 62	imbi12d 326	. . . . . . . . . . . . . . 15
64	63	spv 2114	. . . . . . . . . . . . . 14
65		breq2 4419	. . . . . . . . . . . . . . . . . 18
66	65	notbid 300	. . . . . . . . . . . . . . . . 17
67	66	imbi2d 322	. . . . . . . . . . . . . . . 16
68	67	biimpcd 232	. . . . . . . . . . . . . . 15
69	68	impd 437	. . . . . . . . . . . . . 14 $/\$
70	64, 69	syl 17	. . . . . . . . . . . . 13 $/\$
71		eleq1 2527	. . . . . . . . . . . . . . 15
72		vex 3059	. . . . . . . . . . . . . . . . 17
73	72	brres 5129	. . . . . . . . . . . . . . . 16 $/\$
74		df-br 4416	. . . . . . . . . . . . . . . 16
75	72	ideq 5005	. . . . . . . . . . . . . . . . 17
76	75	anbi1i 706	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	73, 74, 76	3bitr3ri 284	. . . . . . . . . . . . . . 15 $/\$
78	71, 77	syl6bbr 271	. . . . . . . . . . . . . 14 $/\$
79		eleq1 2527	. . . . . . . . . . . . . . . 16
80		df-br 4416	. . . . . . . . . . . . . . . 16
81	79, 80	syl6bbr 271	. . . . . . . . . . . . . . 15
82	81	notbid 300	. . . . . . . . . . . . . 14
83	78, 82	imbi12d 326	. . . . . . . . . . . . 13 $/\$
84	70, 83	syl5ibrcom 230	. . . . . . . . . . . 12
85	84	exlimdvv 1790	. . . . . . . . . . 11
86	85	impd 437	. . . . . . . . . 10 $/\$
87	58, 86	syl5 33	. . . . . . . . 9
88	87	con2d 120	. . . . . . . 8
89	88	alrimiv 1783	. . . . . . 7
90	54, 89	impbii 192	. . . . . 6
91		df-ral 2753	. . . . . 6
92	90, 91	bitr4i 260	. . . . 5
93	35, 36, 92	3bitri 279	. . . 4
94		ralcom 2962	. . . . . . 7 $/\$ $/\$
95		r19.23v 2878	. . . . . . . 8 $/\$ $/\$
96	95	ralbii 2830	. . . . . . 7 $/\$ $/\$
97	94, 96	bitri 257	. . . . . 6 $/\$ $/\$
98	97	ralbii 2830	. . . . 5 $/\$ $/\$
99		brin 4465	. . . . . . . . . . . 12 $/\$
100		brin 4465	. . . . . . . . . . . 12 $/\$
101	99, 100	anbi12i 708	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
102		an4 838	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		ancom 456	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		ancom 456	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	anbi1i 706	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		brxp 4883	. . . . . . . . . . . . . . 15 $/\$
107		brxp 4883	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	anbi12i 708	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109		anandi 842	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 108, 109	3bitr4i 285	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
111	110	anbi1i 706	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 103, 111	3bitri 279	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		anass 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	101, 112, 113	3bitri 279	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
115	114	exbii 1728	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
116	42, 72	brco 5023	. . . . . . . . . 10 $/\$
117		df-br 4416	. . . . . . . . . 10
118	116, 117	bitr3i 259	. . . . . . . . 9 $/\$
119		df-rex 2754	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120		r19.42v 2956	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	119, 120	bitr3i 259	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 118, 121	3bitr3ri 284	. . . . . . . 8 $/\$ $/\$ $/\$
123		df-br 4416	. . . . . . . 8
124	122, 123	imbi12i 332	. . . . . . 7 $/\$ $/\$ $/\$
125	124	2albii 1702	. . . . . 6 $/\$ $/\$ $/\$
126		r2al 2777	. . . . . . 7 $/\$ $/\$ $/\$
127		impexp 452	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	2albii 1702	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
129	126, 128	bitr4i 260	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130		relco 5351	. . . . . . 7
131		ssrel 4941	. . . . . . 7
132	130, 131	ax-mp 5	. . . . . 6
133	125, 129, 132	3bitr4i 285	. . . . 5 $/\$
134	98, 133	bitr2i 258	. . . 4 $/\$
135	93, 134	anbi12i 708	. . 3 $/\$ $/\$ $/\$
136	33, 34, 135	3bitr4g 296	. 2 $/\$
137	26, 136	pm2.61ine 2718	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 375

wal 1452

wceq 1454

wex 1673

wcel 1897

wne 2632

wral 2748

wrex 2749

cvv 3056

cin 3414

wss 3415

c0 3742

cop 3985 class class class wbr 4415

cid 4762

wpo 4771

cxp 4850

cres 4854

ccom 4856

wrel 4857

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-br 4416 df-opab 4475 df-id 4767 df-po 4773 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-res 4864

This theorem is referenced by: (None)

W3C validator