enq0enq - Intuitionistic Logic Explorer

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

Theorem enq0enq 7579

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 7572	. . 3 ~_Q0 $/\$ $/\$ $/\$ $/\$
2		df-xp 4699	. . 3 $/\$
3	1, 2	ineq12i 3380	. 2 ~_Q0 $/\$ $/\$ $/\$ $/\$ $/\$
4		inopab 4828	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		an32 562	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		an4 586	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		pinn 7457	. . . . . . . . . . . . 13
8	7	ssriv 3205	. . . . . . . . . . . 12
9		xpss1 4803	. . . . . . . . . . . 12
10	8, 9	ax-mp 5	. . . . . . . . . . 11
11	10	sseli 3197	. . . . . . . . . 10
12	11	pm4.71ri 392	. . . . . . . . 9 $/\$
13	10	sseli 3197	. . . . . . . . . 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 2270	. . . . . . . . . . . . . . . . . . 19
20		opelxp 4723	. . . . . . . . . . . . . . . . . . 19 $/\$
21	19, 20	bitrdi 196	. . . . . . . . . . . . . . . . . 18 $/\$
22		eleq1 2270	. . . . . . . . . . . . . . . . . . 19
23		opelxp 4723	. . . . . . . . . . . . . . . . . . 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 7465	. . . . . . . . . . . . . . . . . 18 $/\$
31		mulpiord 7465	. . . . . . . . . . . . . . . . . 18 $/\$
32	30, 31	eqeqan12d 2223	. . . . . . . . . . . . . . . . 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 1630	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		19.42vv 1936	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		19.42vv 1936	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	48, 49, 50	3bitr3i 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	51	2exbii 1630	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53		19.42vv 1936	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		19.42vv 1936	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	52, 53, 54	3bitr3i 210	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	18, 55	bitri 184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	opabbii 4127	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		df-enq 7495	. . 3 $/\$ $/\$ $/\$ $/\$
59	57, 58	eqtr4i 2231	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	3, 4, 59	3eqtrri 2233	1 ~_Q0

Colors of variables: wff set class

Syntax hints: $/\$ wa 104

wb 105

wceq 1373

wex 1516

wcel 2178

cin 3173

wss 3174

cop 3646

copab 4120

com 4656

cxp 4691 (class class class)co 5967

comu 6523

cnpi 7420

cmi 7422

ceq 7427 ~_Q0 ceq0 7434

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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-14 2181 ax-ext 2189 ax-sep 4178 ax-pow 4234 ax-pr 4269

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1485 df-sb 1787 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ral 2491 df-rex 2492 df-v 2778 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-br 4060 df-opab 4122 df-xp 4699 df-rel 4700 df-res 4705 df-iota 5251 df-fv 5298 df-ov 5970 df-ni 7452 df-mi 7454 df-enq 7495 df-enq0 7572

This theorem is referenced by: nqnq0pi 7586

W3C validator