Metamath Proof Explorer


Theorem brtrclfv2

Description: Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020)

Ref Expression
Assertion brtrclfv2 X U Y V R W X t+ R Y Y f | R X f f

Proof

Step Hyp Ref Expression
1 df-br X r | R r r r r Y X Y r | R r r r r
2 1 a1i X U Y V R W X r | R r r r r Y X Y r | R r r r r
3 trclfv R W t+ R = r | R r r r r
4 3 breqd R W X t+ R Y X r | R r r r r Y
5 4 3ad2ant3 X U Y V R W X t+ R Y X r | R r r r r Y
6 elimasng X U Y V Y r | R r r r r X X Y r | R r r r r
7 6 3adant3 X U Y V R W Y r | R r r r r X X Y r | R r r r r
8 2 5 7 3bitr4d X U Y V R W X t+ R Y Y r | R r r r r X
9 intimasn X U r | R r r r r X = g | s r | R r r r r g = s X
10 9 3ad2ant1 X U Y V R W r | R r r r r X = g | s r | R r r r r g = s X
11 simpl3 X U Y V R W R X f f R W
12 snex X V
13 vex f V
14 12 13 xpex X × f V
15 unexg R W X × f V R X × f V
16 11 14 15 sylancl X U Y V R W R X f f R X × f V
17 trclfvlb R X × f V R X × f t+ R X × f
18 17 unssad R X × f V R t+ R X × f
19 16 18 syl X U Y V R W R X f f R t+ R X × f
20 trclfvcotrg t+ R X × f t+ R X × f t+ R X × f
21 20 a1i X U Y V R W R X f f t+ R X × f t+ R X × f t+ R X × f
22 simpl1 X U Y V R W R X f f X U
23 snidg X U X X
24 22 23 syl X U Y V R W R X f f X X
25 inelcm X X X X X X
26 24 24 25 syl2anc X U Y V R W R X f f X X
27 xpima2 X X X × f X = f
28 26 27 syl X U Y V R W R X f f X × f X = f
29 16 17 syl X U Y V R W R X f f R X × f t+ R X × f
30 29 unssbd X U Y V R W R X f f X × f t+ R X × f
31 imass1 X × f t+ R X × f X × f X t+ R X × f X
32 30 31 syl X U Y V R W R X f f X × f X t+ R X × f X
33 28 32 eqsstrrd X U Y V R W R X f f f t+ R X × f X
34 imaundir R X × f X f = R X f X × f X f
35 simpr X U Y V R W R X f f R X f f
36 imassrn X × f X f ran X × f
37 rnxpss ran X × f f
38 36 37 sstri X × f X f f
39 38 a1i X U Y V R W R X f f X × f X f f
40 35 39 unssd X U Y V R W R X f f R X f X × f X f f
41 34 40 eqsstrid X U Y V R W R X f f R X × f X f f
42 trclimalb2 R X × f V R X × f X f f t+ R X × f X f
43 16 41 42 syl2anc X U Y V R W R X f f t+ R X × f X f
44 33 43 eqssd X U Y V R W R X f f f = t+ R X × f X
45 sbcan [˙ t+ R X × f / r]˙ R r r r r f = r X [˙ t+ R X × f / r]˙ R r r r r [˙ t+ R X × f / r]˙ f = r X
46 sbcan [˙ t+ R X × f / r]˙ R r r r r [˙ t+ R X × f / r]˙ R r [˙ t+ R X × f / r]˙ r r r
47 fvex t+ R X × f V
48 sbcssg t+ R X × f V [˙ t+ R X × f / r]˙ R r t+ R X × f / r R t+ R X × f / r r
49 47 48 ax-mp [˙ t+ R X × f / r]˙ R r t+ R X × f / r R t+ R X × f / r r
50 csbconstg t+ R X × f V t+ R X × f / r R = R
51 47 50 ax-mp t+ R X × f / r R = R
52 47 csbvargi t+ R X × f / r r = t+ R X × f
53 51 52 sseq12i t+ R X × f / r R t+ R X × f / r r R t+ R X × f
54 49 53 bitri [˙ t+ R X × f / r]˙ R r R t+ R X × f
55 sbcssg t+ R X × f V [˙ t+ R X × f / r]˙ r r r t+ R X × f / r r r t+ R X × f / r r
56 47 55 ax-mp [˙ t+ R X × f / r]˙ r r r t+ R X × f / r r r t+ R X × f / r r
57 csbcog t+ R X × f V t+ R X × f / r r r = t+ R X × f / r r t+ R X × f / r r
58 47 57 ax-mp t+ R X × f / r r r = t+ R X × f / r r t+ R X × f / r r
59 52 52 coeq12i t+ R X × f / r r t+ R X × f / r r = t+ R X × f t+ R X × f
60 58 59 eqtri t+ R X × f / r r r = t+ R X × f t+ R X × f
61 60 52 sseq12i t+ R X × f / r r r t+ R X × f / r r t+ R X × f t+ R X × f t+ R X × f
62 56 61 bitri [˙ t+ R X × f / r]˙ r r r t+ R X × f t+ R X × f t+ R X × f
63 54 62 anbi12i [˙ t+ R X × f / r]˙ R r [˙ t+ R X × f / r]˙ r r r R t+ R X × f t+ R X × f t+ R X × f t+ R X × f
64 46 63 bitri [˙ t+ R X × f / r]˙ R r r r r R t+ R X × f t+ R X × f t+ R X × f t+ R X × f
65 sbceq2g t+ R X × f V [˙ t+ R X × f / r]˙ f = r X f = t+ R X × f / r r X
66 47 65 ax-mp [˙ t+ R X × f / r]˙ f = r X f = t+ R X × f / r r X
67 csbima12 t+ R X × f / r r X = t+ R X × f / r r t+ R X × f / r X
68 52 imaeq1i t+ R X × f / r r t+ R X × f / r X = t+ R X × f t+ R X × f / r X
69 csbconstg t+ R X × f V t+ R X × f / r X = X
70 47 69 ax-mp t+ R X × f / r X = X
71 70 imaeq2i t+ R X × f t+ R X × f / r X = t+ R X × f X
72 67 68 71 3eqtri t+ R X × f / r r X = t+ R X × f X
73 72 eqeq2i f = t+ R X × f / r r X f = t+ R X × f X
74 66 73 bitri [˙ t+ R X × f / r]˙ f = r X f = t+ R X × f X
75 64 74 anbi12i [˙ t+ R X × f / r]˙ R r r r r [˙ t+ R X × f / r]˙ f = r X R t+ R X × f t+ R X × f t+ R X × f t+ R X × f f = t+ R X × f X
76 45 75 sylbbr R t+ R X × f t+ R X × f t+ R X × f t+ R X × f f = t+ R X × f X [˙ t+ R X × f / r]˙ R r r r r f = r X
77 19 21 44 76 syl21anc X U Y V R W R X f f [˙ t+ R X × f / r]˙ R r r r r f = r X
78 77 spesbcd X U Y V R W R X f f r R r r r r f = r X
79 78 ex X U Y V R W R X f f r R r r r r f = r X
80 eqeq1 g = f g = s X f = s X
81 80 rexbidv g = f s r | R r r r r g = s X s r | R r r r r f = s X
82 imaeq1 s = r s X = r X
83 82 eqeq2d s = r f = s X f = r X
84 83 rexab2 s r | R r r r r f = s X r R r r r r f = r X
85 81 84 bitrdi g = f s r | R r r r r g = s X r R r r r r f = r X
86 13 85 elab f g | s r | R r r r r g = s X r R r r r r f = r X
87 79 86 syl6ibr X U Y V R W R X f f f g | s r | R r r r r g = s X
88 intss1 f g | s r | R r r r r g = s X g | s r | R r r r r g = s X f
89 87 88 syl6 X U Y V R W R X f f g | s r | R r r r r g = s X f
90 89 alrimiv X U Y V R W f R X f f g | s r | R r r r r g = s X f
91 ssintab g | s r | R r r r r g = s X f | R X f f f R X f f g | s r | R r r r r g = s X f
92 90 91 sylibr X U Y V R W g | s r | R r r r r g = s X f | R X f f
93 ssintab f | R X f f g | s r | R r r r r g = s X g s r | R r r r r g = s X f | R X f f g
94 82 eqeq2d s = r g = s X g = r X
95 94 rexab2 s r | R r r r r g = s X r R r r r r g = r X
96 simpr R r r r r g = r X g = r X
97 imass1 R r R X r X
98 97 adantr R r r r r R X r X
99 imass1 R r R r X r r X
100 imaco r r X = r r X
101 imass1 r r r r r X r X
102 100 101 eqsstrrid r r r r r X r X
103 99 102 sylan9ss R r r r r R r X r X
104 98 103 jca R r r r r R X r X R r X r X
105 104 adantr R r r r r g = r X R X r X R r X r X
106 vex r V
107 106 imaex r X V
108 imaundi R X f = R X R f
109 108 sseq1i R X f f R X R f f
110 unss R X f R f f R X R f f
111 109 110 bitr4i R X f f R X f R f f
112 imaeq2 f = r X R f = R r X
113 id f = r X f = r X
114 112 113 sseq12d f = r X R f f R r X r X
115 114 cleq2lem f = r X R X f R f f R X r X R r X r X
116 111 115 syl5bb f = r X R X f f R X r X R r X r X
117 107 116 elab r X f | R X f f R X r X R r X r X
118 105 117 sylibr R r r r r g = r X r X f | R X f f
119 96 118 eqeltrd R r r r r g = r X g f | R X f f
120 119 exlimiv r R r r r r g = r X g f | R X f f
121 95 120 sylbi s r | R r r r r g = s X g f | R X f f
122 intss1 g f | R X f f f | R X f f g
123 121 122 syl s r | R r r r r g = s X f | R X f f g
124 93 123 mpgbir f | R X f f g | s r | R r r r r g = s X
125 124 a1i X U Y V R W f | R X f f g | s r | R r r r r g = s X
126 92 125 eqssd X U Y V R W g | s r | R r r r r g = s X = f | R X f f
127 10 126 eqtrd X U Y V R W r | R r r r r X = f | R X f f
128 127 eleq2d X U Y V R W Y r | R r r r r X Y f | R X f f
129 8 128 bitrd X U Y V R W X t+ R Y Y f | R X f f