enq0enq - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > enq0enq		Unicode version

Theorem enq0enq 7421

Description: Equivalence on positive fractions in terms of equivalence on nonnegative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.)

**Assertion**
Ref	Expression
enq0enq	~_Q0

Proof of Theorem enq0enq Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-enq0 7414	. . 3 ~_Q0 $/\$ $/\$ $/\$ $/\$
2		df-xp 4629	. . 3 $/\$
3	1, 2	ineq12i 3334	. 2 ~_Q0 $/\$ $/\$ $/\$ $/\$ $/\$
4		inopab 4755	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		an32 562	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		an4 586	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		pinn 7299	. . . . . . . . . . . . 13
8	7	ssriv 3159	. . . . . . . . . . . 12
9		xpss1 4733	. . . . . . . . . . . 12
10	8, 9	ax-mp 5	. . . . . . . . . . 11
11	10	sseli 3151	. . . . . . . . . 10
12	11	pm4.71ri 392	. . . . . . . . 9 $/\$
13	10	sseli 3151	. . . . . . . . . 10
14	13	pm4.71ri 392	. . . . . . . . 9 $/\$
15	12, 14	anbi12i 460	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
16	6, 15	bitr4i 187	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
17	16	anbi1i 458	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	5, 17	bitri 184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		eleq1 2240	. . . . . . . . . . . . . . . . . . 19
20		opelxp 4653	. . . . . . . . . . . . . . . . . . 19 $/\$
21	19, 20	bitrdi 196	. . . . . . . . . . . . . . . . . 18 $/\$
22		eleq1 2240	. . . . . . . . . . . . . . . . . . 19
23		opelxp 4653	. . . . . . . . . . . . . . . . . . 19 $/\$
24	22, 23	bitrdi 196	. . . . . . . . . . . . . . . . . 18 $/\$
25	21, 24	bi2anan9 606	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
26	25	pm5.32i 454	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	26	anbi1i 458	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		anass 401	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	27, 28	bitri 184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		mulpiord 7307	. . . . . . . . . . . . . . . . . 18 $/\$
31		mulpiord 7307	. . . . . . . . . . . . . . . . . 18 $/\$
32	30, 31	eqeqan12d 2193	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33	32	an42s 589	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
34	33	pm5.32i 454	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	34	anbi2i 457	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	29, 35	bitr4i 187	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		anass 401	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	36, 37	bitr4i 187	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	26	anbi1i 458	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	38, 39	bitr4i 187	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		ancom 266	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	41	anbi1i 458	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	41	anbi1i 458	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	40, 42, 43	3bitr3i 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		anass 401	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		anass 401	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	44, 45, 46	3bitr3i 210	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	47	2exbii 1606	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		19.42vv 1911	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		19.42vv 1911	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	48, 49, 50	3bitr3i 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	51	2exbii 1606	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		19.42vv 1911	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		19.42vv 1911	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	52, 53, 54	3bitr3i 210	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	18, 55	bitri 184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	opabbii 4067	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		df-enq 7337	. . 3 $/\$ $/\$ $/\$ $/\$
59	57, 58	eqtr4i 2201	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	3, 4, 59	3eqtrri 2203	1 ~_Q0

Colors of variables: wff set class

Syntax hints: $/\$ wa 104

wb 105

wceq 1353

wex 1492

wcel 2148

cin 3128

wss 3129

cop 3594

copab 4060

com 4586

cxp 4621 (class class class)co 5869

comu 6409

cnpi 7262

cmi 7264

ceq 7269 ~_Q0 ceq0 7276

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4118 ax-pow 4171 ax-pr 4206

This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-v 2739 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-br 4001 df-opab 4062 df-xp 4629 df-rel 4630 df-res 4635 df-iota 5174 df-fv 5220 df-ov 5872 df-ni 7294 df-mi 7296 df-enq 7337 df-enq0 7414

This theorem is referenced by: nqnq0pi 7428

W3C validator