Metamath Proof Explorer

Theorem isotone2

Description: Two different ways to say subset relation persists across applications of a function. (Contributed by RP, 31-May-2021)

Ref Expression
Assertion isotone2 
|- ( A. a e. ~P A A. b e. ~P A ( a C_ b -> ( F ` a ) C_ ( F ` b ) ) <-> A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( a = c -> ( a C_ b <-> c C_ b ) )
2 fveq2 
 |-  ( a = c -> ( F ` a ) = ( F ` c ) )
3 2 sseq1d 
 |-  ( a = c -> ( ( F ` a ) C_ ( F ` b ) <-> ( F ` c ) C_ ( F ` b ) ) )
4 1 3 imbi12d 
 |-  ( a = c -> ( ( a C_ b -> ( F ` a ) C_ ( F ` b ) ) <-> ( c C_ b -> ( F ` c ) C_ ( F ` b ) ) ) )
5 sseq2 
 |-  ( b = d -> ( c C_ b <-> c C_ d ) )
6 fveq2 
 |-  ( b = d -> ( F ` b ) = ( F ` d ) )
7 6 sseq2d 
 |-  ( b = d -> ( ( F ` c ) C_ ( F ` b ) <-> ( F ` c ) C_ ( F ` d ) ) )
8 5 7 imbi12d 
 |-  ( b = d -> ( ( c C_ b -> ( F ` c ) C_ ( F ` b ) ) <-> ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) ) )
9 4 8 cbvral2vw 
 |-  ( A. a e. ~P A A. b e. ~P A ( a C_ b -> ( F ` a ) C_ ( F ` b ) ) <-> A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) )
10 inss1 
 |-  ( a i^i b ) C_ a
11 inss2 
 |-  ( a i^i b ) C_ b
12 elpwi 
 |-  ( b e. ~P A -> b C_ A )
13 11 12 sstrid 
 |-  ( b e. ~P A -> ( a i^i b ) C_ A )
14 vex 
 |-  b e. _V
15 14 inex2 
 |-  ( a i^i b ) e. _V
16 15 elpw 
 |-  ( ( a i^i b ) e. ~P A <-> ( a i^i b ) C_ A )
17 13 16 sylibr 
 |-  ( b e. ~P A -> ( a i^i b ) e. ~P A )
18 17 ad2antll 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( a i^i b ) e. ~P A )
19 simprl 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> a e. ~P A )
20 simpl 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) )
21 sseq1 
 |-  ( c = ( a i^i b ) -> ( c C_ d <-> ( a i^i b ) C_ d ) )
22 fveq2 
 |-  ( c = ( a i^i b ) -> ( F ` c ) = ( F ` ( a i^i b ) ) )
23 22 sseq1d 
 |-  ( c = ( a i^i b ) -> ( ( F ` c ) C_ ( F ` d ) <-> ( F ` ( a i^i b ) ) C_ ( F ` d ) ) )
24 21 23 imbi12d 
 |-  ( c = ( a i^i b ) -> ( ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) <-> ( ( a i^i b ) C_ d -> ( F ` ( a i^i b ) ) C_ ( F ` d ) ) ) )
25 sseq2 
 |-  ( d = a -> ( ( a i^i b ) C_ d <-> ( a i^i b ) C_ a ) )
26 fveq2 
 |-  ( d = a -> ( F ` d ) = ( F ` a ) )
27 26 sseq2d 
 |-  ( d = a -> ( ( F ` ( a i^i b ) ) C_ ( F ` d ) <-> ( F ` ( a i^i b ) ) C_ ( F ` a ) ) )
28 25 27 imbi12d 
 |-  ( d = a -> ( ( ( a i^i b ) C_ d -> ( F ` ( a i^i b ) ) C_ ( F ` d ) ) <-> ( ( a i^i b ) C_ a -> ( F ` ( a i^i b ) ) C_ ( F ` a ) ) ) )
29 24 28 rspc2va 
 |-  ( ( ( ( a i^i b ) e. ~P A /\ a e. ~P A ) /\ A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) ) -> ( ( a i^i b ) C_ a -> ( F ` ( a i^i b ) ) C_ ( F ` a ) ) )
30 18 19 20 29 syl21anc 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( ( a i^i b ) C_ a -> ( F ` ( a i^i b ) ) C_ ( F ` a ) ) )
31 10 30 mpi 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( F ` ( a i^i b ) ) C_ ( F ` a ) )
32 simprr 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> b e. ~P A )
33 sseq2 
 |-  ( d = b -> ( ( a i^i b ) C_ d <-> ( a i^i b ) C_ b ) )
34 fveq2 
 |-  ( d = b -> ( F ` d ) = ( F ` b ) )
35 34 sseq2d 
 |-  ( d = b -> ( ( F ` ( a i^i b ) ) C_ ( F ` d ) <-> ( F ` ( a i^i b ) ) C_ ( F ` b ) ) )
36 33 35 imbi12d 
 |-  ( d = b -> ( ( ( a i^i b ) C_ d -> ( F ` ( a i^i b ) ) C_ ( F ` d ) ) <-> ( ( a i^i b ) C_ b -> ( F ` ( a i^i b ) ) C_ ( F ` b ) ) ) )
37 24 36 rspc2va 
 |-  ( ( ( ( a i^i b ) e. ~P A /\ b e. ~P A ) /\ A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) ) -> ( ( a i^i b ) C_ b -> ( F ` ( a i^i b ) ) C_ ( F ` b ) ) )
38 18 32 20 37 syl21anc 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( ( a i^i b ) C_ b -> ( F ` ( a i^i b ) ) C_ ( F ` b ) ) )
39 11 38 mpi 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( F ` ( a i^i b ) ) C_ ( F ` b ) )
40 31 39 ssind 
 |-  ( ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) )
41 40 ralrimivva 
 |-  ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) -> A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) )
42 dfss 
 |-  ( c C_ d <-> c = ( c i^i d ) )
43 fveq2 
 |-  ( c = ( c i^i d ) -> ( F ` c ) = ( F ` ( c i^i d ) ) )
44 43 adantl 
 |-  ( ( ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) /\ c = ( c i^i d ) ) -> ( F ` c ) = ( F ` ( c i^i d ) ) )
45 ineq1 
 |-  ( a = c -> ( a i^i b ) = ( c i^i b ) )
46 45 fveq2d 
 |-  ( a = c -> ( F ` ( a i^i b ) ) = ( F ` ( c i^i b ) ) )
47 2 ineq1d 
 |-  ( a = c -> ( ( F ` a ) i^i ( F ` b ) ) = ( ( F ` c ) i^i ( F ` b ) ) )
48 46 47 sseq12d 
 |-  ( a = c -> ( ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) <-> ( F ` ( c i^i b ) ) C_ ( ( F ` c ) i^i ( F ` b ) ) ) )
49 ineq2 
 |-  ( b = d -> ( c i^i b ) = ( c i^i d ) )
50 49 fveq2d 
 |-  ( b = d -> ( F ` ( c i^i b ) ) = ( F ` ( c i^i d ) ) )
51 6 ineq2d 
 |-  ( b = d -> ( ( F ` c ) i^i ( F ` b ) ) = ( ( F ` c ) i^i ( F ` d ) ) )
52 50 51 sseq12d 
 |-  ( b = d -> ( ( F ` ( c i^i b ) ) C_ ( ( F ` c ) i^i ( F ` b ) ) <-> ( F ` ( c i^i d ) ) C_ ( ( F ` c ) i^i ( F ` d ) ) ) )
53 48 52 rspc2va 
 |-  ( ( ( c e. ~P A /\ d e. ~P A ) /\ A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) ) -> ( F ` ( c i^i d ) ) C_ ( ( F ` c ) i^i ( F ` d ) ) )
54 53 ancoms 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( F ` ( c i^i d ) ) C_ ( ( F ` c ) i^i ( F ` d ) ) )
55 inss2 
 |-  ( ( F ` c ) i^i ( F ` d ) ) C_ ( F ` d )
56 54 55 sstrdi 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( F ` ( c i^i d ) ) C_ ( F ` d ) )
57 56 adantr 
 |-  ( ( ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) /\ c = ( c i^i d ) ) -> ( F ` ( c i^i d ) ) C_ ( F ` d ) )
58 44 57 eqsstrd 
 |-  ( ( ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) /\ c = ( c i^i d ) ) -> ( F ` c ) C_ ( F ` d ) )
59 58 ex 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( c = ( c i^i d ) -> ( F ` c ) C_ ( F ` d ) ) )
60 42 59 syl5bi 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) )
61 60 ralrimivva 
 |-  ( A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) -> A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) )
62 41 61 impbii 
 |-  ( A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) <-> A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) )
63 9 62 bitri 
 |-  ( A. a e. ~P A A. b e. ~P A ( a C_ b -> ( F ` a ) C_ ( F ` b ) ) <-> A. a e. ~P A A. b e. ~P A ( F ` ( a i^i b ) ) C_ ( ( F ` a ) i^i ( F ` b ) ) )