Metamath Proof Explorer

Theorem isotone1

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

Ref Expression
Assertion isotone1 
|- ( 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 ) u. ( F ` b ) ) C_ ( F ` ( a u. 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 ssun1 
 |-  a C_ ( a u. b )
11 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 )
12 pwuncl 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( a u. b ) e. ~P A )
13 12 adantl 
 |-  ( ( 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 u. b ) e. ~P A )
14 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 ) ) )
15 sseq1 
 |-  ( c = a -> ( c C_ d <-> a C_ d ) )
16 fveq2 
 |-  ( c = a -> ( F ` c ) = ( F ` a ) )
17 16 sseq1d 
 |-  ( c = a -> ( ( F ` c ) C_ ( F ` d ) <-> ( F ` a ) C_ ( F ` d ) ) )
18 15 17 imbi12d 
 |-  ( c = a -> ( ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) <-> ( a C_ d -> ( F ` a ) C_ ( F ` d ) ) ) )
19 sseq2 
 |-  ( d = ( a u. b ) -> ( a C_ d <-> a C_ ( a u. b ) ) )
20 fveq2 
 |-  ( d = ( a u. b ) -> ( F ` d ) = ( F ` ( a u. b ) ) )
21 20 sseq2d 
 |-  ( d = ( a u. b ) -> ( ( F ` a ) C_ ( F ` d ) <-> ( F ` a ) C_ ( F ` ( a u. b ) ) ) )
22 19 21 imbi12d 
 |-  ( d = ( a u. b ) -> ( ( a C_ d -> ( F ` a ) C_ ( F ` d ) ) <-> ( a C_ ( a u. b ) -> ( F ` a ) C_ ( F ` ( a u. b ) ) ) ) )
23 18 22 rspc2va 
 |-  ( ( ( a e. ~P A /\ ( a u. b ) e. ~P A ) /\ A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) ) -> ( a C_ ( a u. b ) -> ( F ` a ) C_ ( F ` ( a u. b ) ) ) )
24 11 13 14 23 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 C_ ( a u. b ) -> ( F ` a ) C_ ( F ` ( a u. b ) ) ) )
25 10 24 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 ) C_ ( F ` ( a u. b ) ) )
26 ssun2 
 |-  b C_ ( a u. b )
27 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 )
28 sseq1 
 |-  ( c = b -> ( c C_ d <-> b C_ d ) )
29 fveq2 
 |-  ( c = b -> ( F ` c ) = ( F ` b ) )
30 29 sseq1d 
 |-  ( c = b -> ( ( F ` c ) C_ ( F ` d ) <-> ( F ` b ) C_ ( F ` d ) ) )
31 28 30 imbi12d 
 |-  ( c = b -> ( ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) <-> ( b C_ d -> ( F ` b ) C_ ( F ` d ) ) ) )
32 sseq2 
 |-  ( d = ( a u. b ) -> ( b C_ d <-> b C_ ( a u. b ) ) )
33 20 sseq2d 
 |-  ( d = ( a u. b ) -> ( ( F ` b ) C_ ( F ` d ) <-> ( F ` b ) C_ ( F ` ( a u. b ) ) ) )
34 32 33 imbi12d 
 |-  ( d = ( a u. b ) -> ( ( b C_ d -> ( F ` b ) C_ ( F ` d ) ) <-> ( b C_ ( a u. b ) -> ( F ` b ) C_ ( F ` ( a u. b ) ) ) ) )
35 31 34 rspc2va 
 |-  ( ( ( b e. ~P A /\ ( a u. b ) e. ~P A ) /\ A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) ) -> ( b C_ ( a u. b ) -> ( F ` b ) C_ ( F ` ( a u. b ) ) ) )
36 27 13 14 35 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 ) ) -> ( b C_ ( a u. b ) -> ( F ` b ) C_ ( F ` ( a u. b ) ) ) )
37 26 36 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 ` b ) C_ ( F ` ( a u. b ) ) )
38 25 37 unssd 
 |-  ( ( 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 ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) )
39 38 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 ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) )
40 ssequn1 
 |-  ( c C_ d <-> ( c u. d ) = d )
41 2 uneq1d 
 |-  ( a = c -> ( ( F ` a ) u. ( F ` b ) ) = ( ( F ` c ) u. ( F ` b ) ) )
42 uneq1 
 |-  ( a = c -> ( a u. b ) = ( c u. b ) )
43 42 fveq2d 
 |-  ( a = c -> ( F ` ( a u. b ) ) = ( F ` ( c u. b ) ) )
44 41 43 sseq12d 
 |-  ( a = c -> ( ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) <-> ( ( F ` c ) u. ( F ` b ) ) C_ ( F ` ( c u. b ) ) ) )
45 6 uneq2d 
 |-  ( b = d -> ( ( F ` c ) u. ( F ` b ) ) = ( ( F ` c ) u. ( F ` d ) ) )
46 uneq2 
 |-  ( b = d -> ( c u. b ) = ( c u. d ) )
47 46 fveq2d 
 |-  ( b = d -> ( F ` ( c u. b ) ) = ( F ` ( c u. d ) ) )
48 45 47 sseq12d 
 |-  ( b = d -> ( ( ( F ` c ) u. ( F ` b ) ) C_ ( F ` ( c u. b ) ) <-> ( ( F ` c ) u. ( F ` d ) ) C_ ( F ` ( c u. d ) ) ) )
49 44 48 rspc2va 
 |-  ( ( ( c e. ~P A /\ d e. ~P A ) /\ A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) ) -> ( ( F ` c ) u. ( F ` d ) ) C_ ( F ` ( c u. d ) ) )
50 49 ancoms 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( ( F ` c ) u. ( F ` d ) ) C_ ( F ` ( c u. d ) ) )
51 50 unssad 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( F ` c ) C_ ( F ` ( c u. d ) ) )
52 51 adantr 
 |-  ( ( ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) /\ ( c u. d ) = d ) -> ( F ` c ) C_ ( F ` ( c u. d ) ) )
53 fveq2 
 |-  ( ( c u. d ) = d -> ( F ` ( c u. d ) ) = ( F ` d ) )
54 53 adantl 
 |-  ( ( ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) /\ ( c u. d ) = d ) -> ( F ` ( c u. d ) ) = ( F ` d ) )
55 52 54 sseqtrd 
 |-  ( ( ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) /\ ( c u. d ) = d ) -> ( F ` c ) C_ ( F ` d ) )
56 55 ex 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( ( c u. d ) = d -> ( F ` c ) C_ ( F ` d ) ) )
57 40 56 syl5bi 
 |-  ( ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) /\ ( c e. ~P A /\ d e. ~P A ) ) -> ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) )
58 57 ralrimivva 
 |-  ( A. a e. ~P A A. b e. ~P A ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) -> A. c e. ~P A A. d e. ~P A ( c C_ d -> ( F ` c ) C_ ( F ` d ) ) )
59 39 58 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 ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) )
60 9 59 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 ) u. ( F ` b ) ) C_ ( F ` ( a u. b ) ) )