Metamath Proof Explorer

Theorem brttrcl2

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

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

Proof

Step Hyp Ref Expression
1 brttrcl 
 |-  ( A t++ R B <-> E. m e. ( _om \ 1o ) E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) )
2 df-1o 
 |-  1o = suc (/)
3 2 difeq2i 
 |-  ( _om \ 1o ) = ( _om \ suc (/) )
4 3 eleq2i 
 |-  ( m e. ( _om \ 1o ) <-> m e. ( _om \ suc (/) ) )
5 peano1 
 |-  (/) e. _om
6 eldifsucnn 
 |-  ( (/) e. _om -> ( m e. ( _om \ suc (/) ) <-> E. n e. ( _om \ (/) ) m = suc n ) )
7 5 6 ax-mp 
 |-  ( m e. ( _om \ suc (/) ) <-> E. n e. ( _om \ (/) ) m = suc n )
8 dif0 
 |-  ( _om \ (/) ) = _om
9 8 rexeqi 
 |-  ( E. n e. ( _om \ (/) ) m = suc n <-> E. n e. _om m = suc n )
10 4 7 9 3bitri 
 |-  ( m e. ( _om \ 1o ) <-> E. n e. _om m = suc n )
11 10 anbi1i 
 |-  ( ( m e. ( _om \ 1o ) /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) <-> ( E. n e. _om m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) )
12 r19.41v 
 |-  ( E. n e. _om ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) <-> ( E. n e. _om m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) )
13 11 12 bitr4i 
 |-  ( ( m e. ( _om \ 1o ) /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) <-> E. n e. _om ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) )
14 13 exbii 
 |-  ( E. m ( m e. ( _om \ 1o ) /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) <-> E. m E. n e. _om ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) )
15 df-rex 
 |-  ( E. m e. ( _om \ 1o ) E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) <-> E. m ( m e. ( _om \ 1o ) /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) )
16 rexcom4 
 |-  ( E. n e. _om E. m ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) <-> E. m E. n e. _om ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) )
17 14 15 16 3bitr4i 
 |-  ( E. m e. ( _om \ 1o ) E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) <-> E. n e. _om E. m ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) )
18 vex 
 |-  n e. _V
19 18 sucex 
 |-  suc n e. _V
20 suceq 
 |-  ( m = suc n -> suc m = suc suc n )
21 20 fneq2d 
 |-  ( m = suc n -> ( f Fn suc m <-> f Fn suc suc n ) )
22 fveqeq2 
 |-  ( m = suc n -> ( ( f ` m ) = B <-> ( f ` suc n ) = B ) )
23 22 anbi2d 
 |-  ( m = suc n -> ( ( ( f ` (/) ) = A /\ ( f ` m ) = B ) <-> ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) ) )
24 raleq 
 |-  ( m = suc n -> ( A. a e. m ( f ` a ) R ( f ` suc a ) <-> A. a e. suc n ( f ` a ) R ( f ` suc a ) ) )
25 21 23 24 3anbi123d 
 |-  ( m = suc n -> ( ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) <-> ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) )
26 25 exbidv 
 |-  ( m = suc n -> ( E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) <-> E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) )
27 19 26 ceqsexv 
 |-  ( E. m ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) <-> E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) )
28 27 rexbii 
 |-  ( E. n e. _om E. m ( m = suc n /\ E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) )
29 1 17 28 3bitri 
 |-  ( A t++ R B <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) )