Metamath Proof Explorer

Theorem frege133d

Description: If F is a function and A and B both follow X in the transitive closure of F , then (for distinct A and B ) either A follows B or B follows A in the transitive closure of F (or both if it loops). Similar to Proposition 133 of Frege1879 p. 86. Compare with frege133 . (Contributed by RP, 18-Jul-2020)

Ref Expression
Hypotheses frege133d.f 
|- ( ph -> F e. _V )
frege133d.xa 
|- ( ph -> X ( t+ ` F ) A )
frege133d.xb 
|- ( ph -> X ( t+ ` F ) B )
frege133d.fun 
|- ( ph -> Fun F )
Assertion frege133d 
|- ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )

Proof

Step Hyp Ref Expression
1 frege133d.f 
 |-  ( ph -> F e. _V )
2 frege133d.xa 
 |-  ( ph -> X ( t+ ` F ) A )
3 frege133d.xb 
 |-  ( ph -> X ( t+ ` F ) B )
4 frege133d.fun 
 |-  ( ph -> Fun F )
5 funrel 
 |-  ( Fun F -> Rel F )
6 4 5 syl 
 |-  ( ph -> Rel F )
7 reltrclfv 
 |-  ( ( F e. _V /\ Rel F ) -> Rel ( t+ ` F ) )
8 1 6 7 syl2anc 
 |-  ( ph -> Rel ( t+ ` F ) )
9 eliniseg2 
 |-  ( Rel ( t+ ` F ) -> ( X e. ( `' ( t+ ` F ) " { B } ) <-> X ( t+ ` F ) B ) )
10 8 9 syl 
 |-  ( ph -> ( X e. ( `' ( t+ ` F ) " { B } ) <-> X ( t+ ` F ) B ) )
11 3 10 mpbird 
 |-  ( ph -> X e. ( `' ( t+ ` F ) " { B } ) )
12 brrelex2 
 |-  ( ( Rel ( t+ ` F ) /\ X ( t+ ` F ) A ) -> A e. _V )
13 8 2 12 syl2anc 
 |-  ( ph -> A e. _V )
14 un12 
 |-  ( ( `' ( t+ ` F ) " { B } ) u. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) = ( { B } u. ( ( `' ( t+ ` F ) " { B } ) u. ( ( t+ ` F ) " { B } ) ) )
15 14 a1i 
 |-  ( ph -> ( ( `' ( t+ ` F ) " { B } ) u. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) = ( { B } u. ( ( `' ( t+ ` F ) " { B } ) u. ( ( t+ ` F ) " { B } ) ) ) )
16 1 15 4 frege131d 
 |-  ( ph -> ( F " ( ( `' ( t+ ` F ) " { B } ) u. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) ) C_ ( ( `' ( t+ ` F ) " { B } ) u. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) )
17 1 11 13 2 16 frege83d 
 |-  ( ph -> A e. ( ( `' ( t+ ` F ) " { B } ) u. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) )
18 elun 
 |-  ( A e. ( { B } u. ( ( t+ ` F ) " { B } ) ) <-> ( A e. { B } \/ A e. ( ( t+ ` F ) " { B } ) ) )
19 18 orbi2i 
 |-  ( ( A e. ( `' ( t+ ` F ) " { B } ) \/ A e. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) <-> ( A e. ( `' ( t+ ` F ) " { B } ) \/ ( A e. { B } \/ A e. ( ( t+ ` F ) " { B } ) ) ) )
20 elun 
 |-  ( A e. ( ( `' ( t+ ` F ) " { B } ) u. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) <-> ( A e. ( `' ( t+ ` F ) " { B } ) \/ A e. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) )
21 3orass 
 |-  ( ( A e. ( `' ( t+ ` F ) " { B } ) \/ A e. { B } \/ A e. ( ( t+ ` F ) " { B } ) ) <-> ( A e. ( `' ( t+ ` F ) " { B } ) \/ ( A e. { B } \/ A e. ( ( t+ ` F ) " { B } ) ) ) )
22 19 20 21 3bitr4i 
 |-  ( A e. ( ( `' ( t+ ` F ) " { B } ) u. ( { B } u. ( ( t+ ` F ) " { B } ) ) ) <-> ( A e. ( `' ( t+ ` F ) " { B } ) \/ A e. { B } \/ A e. ( ( t+ ` F ) " { B } ) ) )
23 17 22 sylib 
 |-  ( ph -> ( A e. ( `' ( t+ ` F ) " { B } ) \/ A e. { B } \/ A e. ( ( t+ ` F ) " { B } ) ) )
24 eliniseg2 
 |-  ( Rel ( t+ ` F ) -> ( A e. ( `' ( t+ ` F ) " { B } ) <-> A ( t+ ` F ) B ) )
25 8 24 syl 
 |-  ( ph -> ( A e. ( `' ( t+ ` F ) " { B } ) <-> A ( t+ ` F ) B ) )
26 25 biimpd 
 |-  ( ph -> ( A e. ( `' ( t+ ` F ) " { B } ) -> A ( t+ ` F ) B ) )
27 elsni 
 |-  ( A e. { B } -> A = B )
28 27 a1i 
 |-  ( ph -> ( A e. { B } -> A = B ) )
29 elrelimasn 
 |-  ( Rel ( t+ ` F ) -> ( A e. ( ( t+ ` F ) " { B } ) <-> B ( t+ ` F ) A ) )
30 8 29 syl 
 |-  ( ph -> ( A e. ( ( t+ ` F ) " { B } ) <-> B ( t+ ` F ) A ) )
31 30 biimpd 
 |-  ( ph -> ( A e. ( ( t+ ` F ) " { B } ) -> B ( t+ ` F ) A ) )
32 26 28 31 3orim123d 
 |-  ( ph -> ( ( A e. ( `' ( t+ ` F ) " { B } ) \/ A e. { B } \/ A e. ( ( t+ ` F ) " { B } ) ) -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) ) )
33 23 32 mpd 
 |-  ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )