Metamath Proof Explorer

Theorem brttrcl

Description: Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024)

Ref Expression
Assertion brttrcl 
|- ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )

Proof

Step Hyp Ref Expression
1 relttrcl 
 |-  Rel t++ R
2 1 brrelex12i 
 |-  ( A t++ R B -> ( A e. _V /\ B e. _V ) )
3 fvex 
 |-  ( f ` (/) ) e. _V
4 eleq1 
 |-  ( ( f ` (/) ) = A -> ( ( f ` (/) ) e. _V <-> A e. _V ) )
5 3 4 mpbii 
 |-  ( ( f ` (/) ) = A -> A e. _V )
6 fvex 
 |-  ( f ` n ) e. _V
7 eleq1 
 |-  ( ( f ` n ) = B -> ( ( f ` n ) e. _V <-> B e. _V ) )
8 6 7 mpbii 
 |-  ( ( f ` n ) = B -> B e. _V )
9 5 8 anim12i 
 |-  ( ( ( f ` (/) ) = A /\ ( f ` n ) = B ) -> ( A e. _V /\ B e. _V ) )
10 9 3ad2ant2 
 |-  ( ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> ( A e. _V /\ B e. _V ) )
11 10 exlimiv 
 |-  ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> ( A e. _V /\ B e. _V ) )
12 11 rexlimivw 
 |-  ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) -> ( A e. _V /\ B e. _V ) )
13 eqeq2 
 |-  ( x = A -> ( ( f ` (/) ) = x <-> ( f ` (/) ) = A ) )
14 13 anbi1d 
 |-  ( x = A -> ( ( ( f ` (/) ) = x /\ ( f ` n ) = y ) <-> ( ( f ` (/) ) = A /\ ( f ` n ) = y ) ) )
15 14 3anbi2d 
 |-  ( x = A -> ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) <-> ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) )
16 15 exbidv 
 |-  ( x = A -> ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) <-> E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) )
17 16 rexbidv 
 |-  ( x = A -> ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) )
18 eqeq2 
 |-  ( y = B -> ( ( f ` n ) = y <-> ( f ` n ) = B ) )
19 18 anbi2d 
 |-  ( y = B -> ( ( ( f ` (/) ) = A /\ ( f ` n ) = y ) <-> ( ( f ` (/) ) = A /\ ( f ` n ) = B ) ) )
20 19 3anbi2d 
 |-  ( y = B -> ( ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) <-> ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) )
21 20 exbidv 
 |-  ( y = B -> ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) <-> E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) )
22 21 rexbidv 
 |-  ( y = B -> ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) )
23 df-ttrcl 
 |-  t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
24 17 22 23 brabg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) )
25 2 12 24 pm5.21nii 
 |-  ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )