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 30346

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 4732	. . . 4
2		res0 5071	. . . . . . 7
3	2	ineq2i 3604	. . . . . 6
4		in0 3733	. . . . . 6
5	3, 4	eqtri 2450	. . . . 5
6		xp0 5217	. . . . . . . . . 10
7	6	ineq2i 3604	. . . . . . . . 9
8	7, 4	eqtri 2450	. . . . . . . 8
9	8	coeq2i 4957	. . . . . . 7
10		co02 5311	. . . . . . 7
11	9, 10	eqtri 2450	. . . . . 6
12		0ss 3736	. . . . . 6
13	11, 12	eqsstri 3437	. . . . 5
14	5, 13	pm3.2i 456	. . . 4 $/\$
15	1, 14	2th 242	. . 3 $/\$
16		poeq2 4721	. . . 4
17		reseq2 5062	. . . . . . 7
18	17	ineq2d 3607	. . . . . 6
19	18	eqeq1d 2430	. . . . 5
20		xpeq2 4811	. . . . . . . 8
21	20	ineq2d 3607	. . . . . . 7
22	21	coeq2d 4959	. . . . . 6
23	22	sseq1d 3434	. . . . 5
24	19, 23	anbi12d 715	. . . 4 $/\$ $/\$
25	16, 24	bibi12d 322	. . 3 $/\$ $/\$
26	15, 25	mpbiri 236	. 2 $/\$
27		r19.28zv 3837	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
28	27	ralbidv 2804	. . . . . 6 $/\$ $/\$ $/\$ $/\$
29		r19.28zv 3837	. . . . . 6 $/\$ $/\$ $/\$ $/\$
30	28, 29	bitrd 256	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	30	ralbidv 2804	. . . 4 $/\$ $/\$ $/\$ $/\$
32		r19.26 2894	. . . 4 $/\$ $/\$ $/\$ $/\$
33	31, 32	syl6bb 264	. . 3 $/\$ $/\$ $/\$ $/\$
34		df-po 4717	. . 3 $/\$ $/\$
35		disj 3778	. . . . 5
36		df-ral 2719	. . . . 5
37		opex 4628	. . . . . . . . . 10
38		eleq1 2494	. . . . . . . . . . . 12
39		df-br 4367	. . . . . . . . . . . 12
40	38, 39	syl6bbr 266	. . . . . . . . . . 11
41		eleq1 2494	. . . . . . . . . . . . 13
42		vex 3025	. . . . . . . . . . . . . . . 16
43		ididg 4950	. . . . . . . . . . . . . . . 16
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . 15
45	42	brres 5073	. . . . . . . . . . . . . . 15 $/\$
46	44, 45	mpbiran 926	. . . . . . . . . . . . . 14
47		df-br 4367	. . . . . . . . . . . . . 14
48	46, 47	bitr3i 254	. . . . . . . . . . . . 13
49	41, 48	syl6bbr 266	. . . . . . . . . . . 12
50	49	notbid 295	. . . . . . . . . . 11
51	40, 50	imbi12d 321	. . . . . . . . . 10
52	37, 51	spcv 3115	. . . . . . . . 9
53	52	con2d 118	. . . . . . . 8
54	53	alrimiv 1767	. . . . . . 7
55		relres 5094	. . . . . . . . . . . 12
56		elrel 4899	. . . . . . . . . . . 12 $/\$
57	55, 56	mpan 674	. . . . . . . . . . 11
58	57	ancri 554	. . . . . . . . . 10 $/\$
59		eleq1 2494	. . . . . . . . . . . . . . . 16
60		breq12 4371	. . . . . . . . . . . . . . . . . 18 $/\$
61	60	anidms 649	. . . . . . . . . . . . . . . . 17
62	61	notbid 295	. . . . . . . . . . . . . . . 16
63	59, 62	imbi12d 321	. . . . . . . . . . . . . . 15
64	63	spv 2076	. . . . . . . . . . . . . 14
65		breq2 4370	. . . . . . . . . . . . . . . . . 18
66	65	notbid 295	. . . . . . . . . . . . . . . . 17
67	66	imbi2d 317	. . . . . . . . . . . . . . . 16
68	67	biimpcd 227	. . . . . . . . . . . . . . 15
69	68	impd 432	. . . . . . . . . . . . . 14 $/\$
70	64, 69	syl 17	. . . . . . . . . . . . 13 $/\$
71		eleq1 2494	. . . . . . . . . . . . . . 15
72		vex 3025	. . . . . . . . . . . . . . . . 17
73	72	brres 5073	. . . . . . . . . . . . . . . 16 $/\$
74		df-br 4367	. . . . . . . . . . . . . . . 16
75	72	ideq 4949	. . . . . . . . . . . . . . . . 17
76	75	anbi1i 699	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	73, 74, 76	3bitr3ri 279	. . . . . . . . . . . . . . 15 $/\$
78	71, 77	syl6bbr 266	. . . . . . . . . . . . . 14 $/\$
79		eleq1 2494	. . . . . . . . . . . . . . . 16
80		df-br 4367	. . . . . . . . . . . . . . . 16
81	79, 80	syl6bbr 266	. . . . . . . . . . . . . . 15
82	81	notbid 295	. . . . . . . . . . . . . 14
83	78, 82	imbi12d 321	. . . . . . . . . . . . 13 $/\$
84	70, 83	syl5ibrcom 225	. . . . . . . . . . . 12
85	84	exlimdvv 1773	. . . . . . . . . . 11
86	85	impd 432	. . . . . . . . . 10 $/\$
87	58, 86	syl5 33	. . . . . . . . 9
88	87	con2d 118	. . . . . . . 8
89	88	alrimiv 1767	. . . . . . 7
90	54, 89	impbii 190	. . . . . 6
91		df-ral 2719	. . . . . 6
92	90, 91	bitr4i 255	. . . . 5
93	35, 36, 92	3bitri 274	. . . 4
94		ralcom 2928	. . . . . . 7 $/\$ $/\$
95		r19.23v 2844	. . . . . . . 8 $/\$ $/\$
96	95	ralbii 2796	. . . . . . 7 $/\$ $/\$
97	94, 96	bitri 252	. . . . . 6 $/\$ $/\$
98	97	ralbii 2796	. . . . 5 $/\$ $/\$
99		brin 4416	. . . . . . . . . . . 12 $/\$
100		brin 4416	. . . . . . . . . . . 12 $/\$
101	99, 100	anbi12i 701	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
102		an4 831	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		ancom 451	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		ancom 451	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	anbi1i 699	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		brxp 4827	. . . . . . . . . . . . . . 15 $/\$
107		brxp 4827	. . . . . . . . . . . . . . 15 $/\$
108	106, 107	anbi12i 701	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109		anandi 835	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
110	105, 108, 109	3bitr4i 280	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
111	110	anbi1i 699	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	102, 103, 111	3bitri 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		anass 653	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	101, 112, 113	3bitri 274	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
115	114	exbii 1712	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
116	42, 72	brco 4967	. . . . . . . . . 10 $/\$
117		df-br 4367	. . . . . . . . . 10
118	116, 117	bitr3i 254	. . . . . . . . 9 $/\$
119		df-rex 2720	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120		r19.42v 2922	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	119, 120	bitr3i 254	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 118, 121	3bitr3ri 279	. . . . . . . 8 $/\$ $/\$ $/\$
123		df-br 4367	. . . . . . . 8
124	122, 123	imbi12i 327	. . . . . . 7 $/\$ $/\$ $/\$
125	124	2albii 1686	. . . . . 6 $/\$ $/\$ $/\$
126		r2al 2743	. . . . . . 7 $/\$ $/\$ $/\$
127		impexp 447	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	2albii 1686	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
129	126, 128	bitr4i 255	. . . . . 6 $/\$ $/\$ $/\$ $/\$
130		relco 5295	. . . . . . 7
131		ssrel 4885	. . . . . . 7
132	130, 131	ax-mp 5	. . . . . 6
133	125, 129, 132	3bitr4i 280	. . . . 5 $/\$
134	98, 133	bitr2i 253	. . . 4 $/\$
135	93, 134	anbi12i 701	. . 3 $/\$ $/\$ $/\$
136	33, 34, 135	3bitr4g 291	. 2 $/\$
137	26, 136	pm2.61ine 2684	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370

wal 1435

wceq 1437

wex 1657

wcel 1872

wne 2599

wral 2714

wrex 2715

cvv 3022

cin 3378

wss 3379

c0 3704

cop 3947 class class class wbr 4366

cid 4706

wpo 4715

cxp 4794

cres 4798

ccom 4800

wrel 4801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408 ax-sep 4489 ax-nul 4498 ax-pr 4603

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-ral 2719 df-rex 2720 df-rab 2723 df-v 3024 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-nul 3705 df-if 3855 df-sn 3942 df-pr 3944 df-op 3948 df-br 4367 df-opab 4426 df-id 4711 df-po 4717 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-res 4808

This theorem is referenced by: (None)

W3C validator