Metamath Proof Explorer

Theorem ntrk1k3eqk13

Description: An interior function is both monotone and sub-linear if and only if it is finitely linear. (Contributed by RP, 18-Jun-2021)

Ref Expression
Assertion ntrk1k3eqk13 
|- ( ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) /\ A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) <-> A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) )

Proof

Step Hyp Ref Expression
1 r19.26-2 
 |-  ( A. s e. ~P B A. t e. ~P B ( ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) /\ ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) <-> ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) /\ A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) )
2 eqss 
 |-  ( ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> ( ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) /\ ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) )
3 2 2ralbii 
 |-  ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. s e. ~P B A. t e. ~P B ( ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) /\ ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) )
4 isotone2 
 |-  ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) )
5 4 anbi1i 
 |-  ( ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) /\ A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) <-> ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) C_ ( ( I ` s ) i^i ( I ` t ) ) /\ A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) )
6 1 3 5 3bitr4ri 
 |-  ( ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) /\ A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) ) <-> A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) )