Theorem trer 15361

Description: A relation intersected with its converse is an equivalence relation if the relation is transitive.

Assertion

Ref	Expression
trer	|- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> Er (R i^i `'R))

Distinct variable group:   a,b,c,R

Proof of Theorem trer

Step	Hyp	Ref	Expression
1		breq1 3341	. . . . . . . . . . . . 13 |- (a = r -> (aRb <-> rRb))
2	1	anbi1d 679	. . . . . . . . . . . 12 |- (a = r -> ((aRb /\ bRc) <-> (rRb /\ bRc)))
3		breq1 3341	. . . . . . . . . . . 12 |- (a = r -> (aRc <-> rRc))
4	2, 3	imbi12d 688	. . . . . . . . . . 11 |- (a = r -> (((aRb /\ bRc) -> aRc) <-> ((rRb /\ bRc) -> rRc)))
5	4	2albidv 1658	. . . . . . . . . 10 |- (a = r -> (A.bA.c((aRb /\ bRc) -> aRc) <-> A.bA.c((rRb /\ bRc) -> rRc)))
6	5	a4v 1649	. . . . . . . . 9 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> A.bA.c((rRb /\ bRc) -> rRc))
7		breq2 3342	. . . . . . . . . . . . 13 |- (b = s -> (rRb <-> rRs))
8		breq1 3341	. . . . . . . . . . . . 13 |- (b = s -> (bRc <-> sRc))
9	7, 8	anbi12d 690	. . . . . . . . . . . 12 |- (b = s -> ((rRb /\ bRc) <-> (rRs /\ sRc)))
10	9	imbi1d 675	. . . . . . . . . . 11 |- (b = s -> (((rRb /\ bRc) -> rRc) <-> ((rRs /\ sRc) -> rRc)))
11	10	albidv 1656	. . . . . . . . . 10 |- (b = s -> (A.c((rRb /\ bRc) -> rRc) <-> A.c((rRs /\ sRc) -> rRc)))
12	11	a4v 1649	. . . . . . . . 9 |- (A.bA.c((rRb /\ bRc) -> rRc) -> A.c((rRs /\ sRc) -> rRc))
13		breq2 3342	. . . . . . . . . . . . 13 |- (c = t -> (sRc <-> sRt))
14	13	anbi2d 678	. . . . . . . . . . . 12 |- (c = t -> ((rRs /\ sRc) <-> (rRs /\ sRt)))
15		breq2 3342	. . . . . . . . . . . 12 |- (c = t -> (rRc <-> rRt))
16	14, 15	imbi12d 688	. . . . . . . . . . 11 |- (c = t -> (((rRs /\ sRc) -> rRc) <-> ((rRs /\ sRt) -> rRt)))
17	16	a4v 1649	. . . . . . . . . 10 |- (A.c((rRs /\ sRc) -> rRc) -> ((rRs /\ sRt) -> rRt))
18		pm3.3 375	. . . . . . . . . . . . . . 15 |- (((rRs /\ sRt) -> rRt) -> (rRs -> (sRt -> rRt)))
19	18	com23 36	. . . . . . . . . . . . . 14 |- (((rRs /\ sRt) -> rRt) -> (sRt -> (rRs -> rRt)))
20	19	adantrd 427	. . . . . . . . . . . . 13 |- (((rRs /\ sRt) -> rRt) -> ((sRt /\ tRs) -> (rRs -> rRt)))
21	20	com23 36	. . . . . . . . . . . 12 |- (((rRs /\ sRt) -> rRt) -> (rRs -> ((sRt /\ tRs) -> rRt)))
22	21	adantrd 427	. . . . . . . . . . 11 |- (((rRs /\ sRt) -> rRt) -> ((rRs /\ sRr) -> ((sRt /\ tRs) -> rRt)))
23	22	imp3a 388	. . . . . . . . . 10 |- (((rRs /\ sRt) -> rRt) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> rRt))
24	17, 23	syl 12	. . . . . . . . 9 |- (A.c((rRs /\ sRc) -> rRc) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> rRt))
25	6, 12, 24	3syl 24	. . . . . . . 8 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> rRt))
26		breq1 3341	. . . . . . . . . . . . 13 |- (a = t -> (aRb <-> tRb))
27	26	anbi1d 679	. . . . . . . . . . . 12 |- (a = t -> ((aRb /\ bRc) <-> (tRb /\ bRc)))
28		breq1 3341	. . . . . . . . . . . 12 |- (a = t -> (aRc <-> tRc))
29	27, 28	imbi12d 688	. . . . . . . . . . 11 |- (a = t -> (((aRb /\ bRc) -> aRc) <-> ((tRb /\ bRc) -> tRc)))
30	29	2albidv 1658	. . . . . . . . . 10 |- (a = t -> (A.bA.c((aRb /\ bRc) -> aRc) <-> A.bA.c((tRb /\ bRc) -> tRc)))
31	30	a4v 1649	. . . . . . . . 9 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> A.bA.c((tRb /\ bRc) -> tRc))
32		breq2 3342	. . . . . . . . . . . . 13 |- (b = s -> (tRb <-> tRs))
33	32, 8	anbi12d 690	. . . . . . . . . . . 12 |- (b = s -> ((tRb /\ bRc) <-> (tRs /\ sRc)))
34	33	imbi1d 675	. . . . . . . . . . 11 |- (b = s -> (((tRb /\ bRc) -> tRc) <-> ((tRs /\ sRc) -> tRc)))
35	34	albidv 1656	. . . . . . . . . 10 |- (b = s -> (A.c((tRb /\ bRc) -> tRc) <-> A.c((tRs /\ sRc) -> tRc)))
36	35	a4v 1649	. . . . . . . . 9 |- (A.bA.c((tRb /\ bRc) -> tRc) -> A.c((tRs /\ sRc) -> tRc))
37		breq2 3342	. . . . . . . . . . . . 13 |- (c = r -> (sRc <-> sRr))
38	37	anbi2d 678	. . . . . . . . . . . 12 |- (c = r -> ((tRs /\ sRc) <-> (tRs /\ sRr)))
39		breq2 3342	. . . . . . . . . . . 12 |- (c = r -> (tRc <-> tRr))
40	38, 39	imbi12d 688	. . . . . . . . . . 11 |- (c = r -> (((tRs /\ sRc) -> tRc) <-> ((tRs /\ sRr) -> tRr)))
41	40	a4v 1649	. . . . . . . . . 10 |- (A.c((tRs /\ sRc) -> tRc) -> ((tRs /\ sRr) -> tRr))
42		pm3.3 375	. . . . . . . . . . . . . 14 |- (((tRs /\ sRr) -> tRr) -> (tRs -> (sRr -> tRr)))
43	42	adantld 426	. . . . . . . . . . . . 13 |- (((tRs /\ sRr) -> tRr) -> ((sRt /\ tRs) -> (sRr -> tRr)))
44	43	com23 36	. . . . . . . . . . . 12 |- (((tRs /\ sRr) -> tRr) -> (sRr -> ((sRt /\ tRs) -> tRr)))
45	44	adantld 426	. . . . . . . . . . 11 |- (((tRs /\ sRr) -> tRr) -> ((rRs /\ sRr) -> ((sRt /\ tRs) -> tRr)))
46	45	imp3a 388	. . . . . . . . . 10 |- (((tRs /\ sRr) -> tRr) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> tRr))
47	41, 46	syl 12	. . . . . . . . 9 |- (A.c((tRs /\ sRc) -> tRc) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> tRr))
48	31, 36, 47	3syl 24	. . . . . . . 8 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> tRr))
49	25, 48	jcad 661	. . . . . . 7 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> (rRt /\ tRr)))
50		brin 3388	. . . . . . . 8 |- (r(R i^i `'R)t <-> (rRt /\ r`'Rt))
51		visset 2295	. . . . . . . . . 10 |- r e. _V
52		visset 2295	. . . . . . . . . 10 |- t e. _V
53	51, 52	brcnv 4144	. . . . . . . . 9 |- (r`'Rt <-> tRr)
54	53	anbi2i 538	. . . . . . . 8 |- ((rRt /\ r`'Rt) <-> (rRt /\ tRr))
55	50, 54	bitr2i 191	. . . . . . 7 |- ((rRt /\ tRr) <-> r(R i^i `'R)t)
56	49, 55	syl6ib 229	. . . . . 6 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> (((rRs /\ sRr) /\ (sRt /\ tRs)) -> r(R i^i `'R)t))
57		brin 3388	. . . . . . . 8 |- (r(R i^i `'R)s <-> (rRs /\ r`'Rs))
58		visset 2295	. . . . . . . . . 10 |- s e. _V
59	51, 58	brcnv 4144	. . . . . . . . 9 |- (r`'Rs <-> sRr)
60	59	anbi2i 538	. . . . . . . 8 |- ((rRs /\ r`'Rs) <-> (rRs /\ sRr))
61	57, 60	bitri 190	. . . . . . 7 |- (r(R i^i `'R)s <-> (rRs /\ sRr))
62		brin 3388	. . . . . . . 8 |- (s(R i^i `'R)t <-> (sRt /\ s`'Rt))
63	58, 52	brcnv 4144	. . . . . . . . 9 |- (s`'Rt <-> tRs)
64	63	anbi2i 538	. . . . . . . 8 |- ((sRt /\ s`'Rt) <-> (sRt /\ tRs))
65	62, 64	bitri 190	. . . . . . 7 |- (s(R i^i `'R)t <-> (sRt /\ tRs))
66	61, 65	anbi12i 540	. . . . . 6 |- ((r(R i^i `'R)s /\ s(R i^i `'R)t) <-> ((rRs /\ sRr) /\ (sRt /\ tRs)))
67	56, 66	syl5ib 223	. . . . 5 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> ((r(R i^i `'R)s /\ s(R i^i `'R)t) -> r(R i^i `'R)t))
68		ancom 482	. . . . . . . 8 |- ((rRs /\ r`'Rs) <-> (r`'Rs /\ rRs))
69	58, 51	brcnv 4144	. . . . . . . . . 10 |- (s`'Rr <-> rRs)
70	69	bicomi 189	. . . . . . . . 9 |- (rRs <-> s`'Rr)
71	59, 70	anbi12i 540	. . . . . . . 8 |- ((r`'Rs /\ rRs) <-> (sRr /\ s`'Rr))
72	68, 71	bitri 190	. . . . . . 7 |- ((rRs /\ r`'Rs) <-> (sRr /\ s`'Rr))
73		brin 3388	. . . . . . 7 |- (s(R i^i `'R)r <-> (sRr /\ s`'Rr))
74	72, 57, 73	3bitr4i 200	. . . . . 6 |- (r(R i^i `'R)s <-> s(R i^i `'R)r)
75	74	biimpi 168	. . . . 5 |- (r(R i^i `'R)s -> s(R i^i `'R)r)
76	67, 75	jctil 316	. . . 4 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> ((r(R i^i `'R)s -> s(R i^i `'R)r) /\ ((r(R i^i `'R)s /\ s(R i^i `'R)t) -> r(R i^i `'R)t)))
77	76	19.21aiv 1664	. . 3 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> A.t((r(R i^i `'R)s -> s(R i^i `'R)r) /\ ((r(R i^i `'R)s /\ s(R i^i `'R)t) -> r(R i^i `'R)t)))
78	77	19.21aivv 1665	. 2 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> A.rA.sA.t((r(R i^i `'R)s -> s(R i^i `'R)r) /\ ((r(R i^i `'R)s /\ s(R i^i `'R)t) -> r(R i^i `'R)t)))
79		dfer2 5319	. 2 |- (Er (R i^i `'R) <-> A.rA.sA.t((r(R i^i `'R)s -> s(R i^i `'R)r) /\ ((r(R i^i `'R)s /\ s(R i^i `'R)t) -> r(R i^i `'R)t)))
80	78, 79	sylibr 217	1 |- (A.aA.bA.c((aRb /\ bRc) -> aRc) -> Er (R i^i `'R))

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   i^i cin 2592   class class class wbr 3338  `'ccnv 3985  Er wer 5315

This theorem is referenced by:  fneer 15496

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-er 5318

Copyright terms: Public domain