enq0enq - Intuitionistic Logic Explorer

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

Theorem enq0enq 7650

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 7643	. . 3 ~_Q0 $/\$ $/\$ $/\$ $/\$
2		df-xp 4731	. . 3 $/\$
3	1, 2	ineq12i 3406	. 2 ~_Q0 $/\$ $/\$ $/\$ $/\$ $/\$
4		inopab 4862	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		an32 564	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		an4 588	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		pinn 7528	. . . . . . . . . . . . 13
8	7	ssriv 3231	. . . . . . . . . . . 12
9		xpss1 4836	. . . . . . . . . . . 12
10	8, 9	ax-mp 5	. . . . . . . . . . 11
11	10	sseli 3223	. . . . . . . . . 10
12	11	pm4.71ri 392	. . . . . . . . 9 $/\$
13	10	sseli 3223	. . . . . . . . . 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 2294	. . . . . . . . . . . . . . . . . . 19
20		opelxp 4755	. . . . . . . . . . . . . . . . . . 19 $/\$
21	19, 20	bitrdi 196	. . . . . . . . . . . . . . . . . 18 $/\$
22		eleq1 2294	. . . . . . . . . . . . . . . . . . 19
23		opelxp 4755	. . . . . . . . . . . . . . . . . . 19 $/\$
24	22, 23	bitrdi 196	. . . . . . . . . . . . . . . . . 18 $/\$
25	21, 24	bi2anan9 610	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
26	25	pm5.32i 454	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	26	anbi1i 458	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		anass 401	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	27, 28	bitri 184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		mulpiord 7536	. . . . . . . . . . . . . . . . . 18 $/\$
31		mulpiord 7536	. . . . . . . . . . . . . . . . . 18 $/\$
32	30, 31	eqeqan12d 2247	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33	32	an42s 593	. . . . . . . . . . . . . . . 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 1654	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		19.42vv 1960	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		19.42vv 1960	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	48, 49, 50	3bitr3i 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	51	2exbii 1654	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		19.42vv 1960	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		19.42vv 1960	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	52, 53, 54	3bitr3i 210	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	18, 55	bitri 184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	opabbii 4156	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		df-enq 7566	. . 3 $/\$ $/\$ $/\$ $/\$
59	57, 58	eqtr4i 2255	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	3, 4, 59	3eqtrri 2257	1 ~_Q0

Colors of variables: wff set class

Syntax hints: $/\$ wa 104

wb 105

wceq 1397

wex 1540

wcel 2202

cin 3199

wss 3200

cop 3672

copab 4149

com 4688

cxp 4723 (class class class)co 6017

comu 6579

cnpi 7491

cmi 7493

ceq 7498 ~_Q0 ceq0 7505

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-v 2804 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-br 4089 df-opab 4151 df-xp 4731 df-rel 4732 df-res 4737 df-iota 5286 df-fv 5334 df-ov 6020 df-ni 7523 df-mi 7525 df-enq 7566 df-enq0 7643

This theorem is referenced by: nqnq0pi 7657

W3C validator