Metamath Proof Explorer

Theorem ipodrsima

Description: The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypotheses ipodrsima.f 
|- ( ph -> F Fn ~P A )
ipodrsima.m 
|- ( ( ph /\ ( u C_ v /\ v C_ A ) ) -> ( F ` u ) C_ ( F ` v ) )
ipodrsima.d 
|- ( ph -> ( toInc ` B ) e. Dirset )
ipodrsima.s 
|- ( ph -> B C_ ~P A )
ipodrsima.a 
|- ( ph -> ( F " B ) e. V )
Assertion ipodrsima 
|- ( ph -> ( toInc ` ( F " B ) ) e. Dirset )

Proof

Step Hyp Ref Expression
1 ipodrsima.f 
 |-  ( ph -> F Fn ~P A )
2 ipodrsima.m 
 |-  ( ( ph /\ ( u C_ v /\ v C_ A ) ) -> ( F ` u ) C_ ( F ` v ) )
3 ipodrsima.d 
 |-  ( ph -> ( toInc ` B ) e. Dirset )
4 ipodrsima.s 
 |-  ( ph -> B C_ ~P A )
5 ipodrsima.a 
 |-  ( ph -> ( F " B ) e. V )
6 5 elexd 
 |-  ( ph -> ( F " B ) e. _V )
7 isipodrs 
 |-  ( ( toInc ` B ) e. Dirset <-> ( B e. _V /\ B =/= (/) /\ A. a e. B A. b e. B E. c e. B ( a u. b ) C_ c ) )
8 3 7 sylib 
 |-  ( ph -> ( B e. _V /\ B =/= (/) /\ A. a e. B A. b e. B E. c e. B ( a u. b ) C_ c ) )
9 8 simp2d 
 |-  ( ph -> B =/= (/) )
10 fnimaeq0 
 |-  ( ( F Fn ~P A /\ B C_ ~P A ) -> ( ( F " B ) = (/) <-> B = (/) ) )
11 1 4 10 syl2anc 
 |-  ( ph -> ( ( F " B ) = (/) <-> B = (/) ) )
12 11 necon3bid 
 |-  ( ph -> ( ( F " B ) =/= (/) <-> B =/= (/) ) )
13 9 12 mpbird 
 |-  ( ph -> ( F " B ) =/= (/) )
14 8 simp3d 
 |-  ( ph -> A. a e. B A. b e. B E. c e. B ( a u. b ) C_ c )
15 simplll 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ a C_ c ) -> ph )
16 simpr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ a C_ c ) -> a C_ c )
17 4 ad2antrr 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> B C_ ~P A )
18 simprr 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> c e. B )
19 17 18 sseldd 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> c e. ~P A )
20 19 elpwid 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> c C_ A )
21 20 adantr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ a C_ c ) -> c C_ A )
22 vex 
 |-  a e. _V
23 vex 
 |-  c e. _V
24 sseq12 
 |-  ( ( u = a /\ v = c ) -> ( u C_ v <-> a C_ c ) )
25 sseq1 
 |-  ( v = c -> ( v C_ A <-> c C_ A ) )
26 25 adantl 
 |-  ( ( u = a /\ v = c ) -> ( v C_ A <-> c C_ A ) )
27 24 26 anbi12d 
 |-  ( ( u = a /\ v = c ) -> ( ( u C_ v /\ v C_ A ) <-> ( a C_ c /\ c C_ A ) ) )
28 27 anbi2d 
 |-  ( ( u = a /\ v = c ) -> ( ( ph /\ ( u C_ v /\ v C_ A ) ) <-> ( ph /\ ( a C_ c /\ c C_ A ) ) ) )
29 fveq2 
 |-  ( u = a -> ( F ` u ) = ( F ` a ) )
30 fveq2 
 |-  ( v = c -> ( F ` v ) = ( F ` c ) )
31 sseq12 
 |-  ( ( ( F ` u ) = ( F ` a ) /\ ( F ` v ) = ( F ` c ) ) -> ( ( F ` u ) C_ ( F ` v ) <-> ( F ` a ) C_ ( F ` c ) ) )
32 29 30 31 syl2an 
 |-  ( ( u = a /\ v = c ) -> ( ( F ` u ) C_ ( F ` v ) <-> ( F ` a ) C_ ( F ` c ) ) )
33 28 32 imbi12d 
 |-  ( ( u = a /\ v = c ) -> ( ( ( ph /\ ( u C_ v /\ v C_ A ) ) -> ( F ` u ) C_ ( F ` v ) ) <-> ( ( ph /\ ( a C_ c /\ c C_ A ) ) -> ( F ` a ) C_ ( F ` c ) ) ) )
34 22 23 33 2 vtocl2 
 |-  ( ( ph /\ ( a C_ c /\ c C_ A ) ) -> ( F ` a ) C_ ( F ` c ) )
35 15 16 21 34 syl12anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ a C_ c ) -> ( F ` a ) C_ ( F ` c ) )
36 35 ex 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> ( a C_ c -> ( F ` a ) C_ ( F ` c ) ) )
37 simplll 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ b C_ c ) -> ph )
38 simpr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ b C_ c ) -> b C_ c )
39 20 adantr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ b C_ c ) -> c C_ A )
40 vex 
 |-  b e. _V
41 sseq12 
 |-  ( ( u = b /\ v = c ) -> ( u C_ v <-> b C_ c ) )
42 25 adantl 
 |-  ( ( u = b /\ v = c ) -> ( v C_ A <-> c C_ A ) )
43 41 42 anbi12d 
 |-  ( ( u = b /\ v = c ) -> ( ( u C_ v /\ v C_ A ) <-> ( b C_ c /\ c C_ A ) ) )
44 43 anbi2d 
 |-  ( ( u = b /\ v = c ) -> ( ( ph /\ ( u C_ v /\ v C_ A ) ) <-> ( ph /\ ( b C_ c /\ c C_ A ) ) ) )
45 fveq2 
 |-  ( u = b -> ( F ` u ) = ( F ` b ) )
46 sseq12 
 |-  ( ( ( F ` u ) = ( F ` b ) /\ ( F ` v ) = ( F ` c ) ) -> ( ( F ` u ) C_ ( F ` v ) <-> ( F ` b ) C_ ( F ` c ) ) )
47 45 30 46 syl2an 
 |-  ( ( u = b /\ v = c ) -> ( ( F ` u ) C_ ( F ` v ) <-> ( F ` b ) C_ ( F ` c ) ) )
48 44 47 imbi12d 
 |-  ( ( u = b /\ v = c ) -> ( ( ( ph /\ ( u C_ v /\ v C_ A ) ) -> ( F ` u ) C_ ( F ` v ) ) <-> ( ( ph /\ ( b C_ c /\ c C_ A ) ) -> ( F ` b ) C_ ( F ` c ) ) ) )
49 40 23 48 2 vtocl2 
 |-  ( ( ph /\ ( b C_ c /\ c C_ A ) ) -> ( F ` b ) C_ ( F ` c ) )
50 37 38 39 49 syl12anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) /\ b C_ c ) -> ( F ` b ) C_ ( F ` c ) )
51 50 ex 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> ( b C_ c -> ( F ` b ) C_ ( F ` c ) ) )
52 36 51 anim12d 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> ( ( a C_ c /\ b C_ c ) -> ( ( F ` a ) C_ ( F ` c ) /\ ( F ` b ) C_ ( F ` c ) ) ) )
53 unss 
 |-  ( ( a C_ c /\ b C_ c ) <-> ( a u. b ) C_ c )
54 unss 
 |-  ( ( ( F ` a ) C_ ( F ` c ) /\ ( F ` b ) C_ ( F ` c ) ) <-> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
55 52 53 54 3imtr3g 
 |-  ( ( ( ph /\ a e. B ) /\ ( b e. B /\ c e. B ) ) -> ( ( a u. b ) C_ c -> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
56 55 anassrs 
 |-  ( ( ( ( ph /\ a e. B ) /\ b e. B ) /\ c e. B ) -> ( ( a u. b ) C_ c -> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
57 56 reximdva 
 |-  ( ( ( ph /\ a e. B ) /\ b e. B ) -> ( E. c e. B ( a u. b ) C_ c -> E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
58 57 ralimdva 
 |-  ( ( ph /\ a e. B ) -> ( A. b e. B E. c e. B ( a u. b ) C_ c -> A. b e. B E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
59 58 ralimdva 
 |-  ( ph -> ( A. a e. B A. b e. B E. c e. B ( a u. b ) C_ c -> A. a e. B A. b e. B E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
60 14 59 mpd 
 |-  ( ph -> A. a e. B A. b e. B E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
61 uneq1 
 |-  ( x = ( F ` a ) -> ( x u. y ) = ( ( F ` a ) u. y ) )
62 61 sseq1d 
 |-  ( x = ( F ` a ) -> ( ( x u. y ) C_ z <-> ( ( F ` a ) u. y ) C_ z ) )
63 62 rexbidv 
 |-  ( x = ( F ` a ) -> ( E. z e. ( F " B ) ( x u. y ) C_ z <-> E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z ) )
64 63 ralbidv 
 |-  ( x = ( F ` a ) -> ( A. y e. ( F " B ) E. z e. ( F " B ) ( x u. y ) C_ z <-> A. y e. ( F " B ) E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z ) )
65 64 ralima 
 |-  ( ( F Fn ~P A /\ B C_ ~P A ) -> ( A. x e. ( F " B ) A. y e. ( F " B ) E. z e. ( F " B ) ( x u. y ) C_ z <-> A. a e. B A. y e. ( F " B ) E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z ) )
66 1 4 65 syl2anc 
 |-  ( ph -> ( A. x e. ( F " B ) A. y e. ( F " B ) E. z e. ( F " B ) ( x u. y ) C_ z <-> A. a e. B A. y e. ( F " B ) E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z ) )
67 uneq2 
 |-  ( y = ( F ` b ) -> ( ( F ` a ) u. y ) = ( ( F ` a ) u. ( F ` b ) ) )
68 67 sseq1d 
 |-  ( y = ( F ` b ) -> ( ( ( F ` a ) u. y ) C_ z <-> ( ( F ` a ) u. ( F ` b ) ) C_ z ) )
69 68 rexbidv 
 |-  ( y = ( F ` b ) -> ( E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z <-> E. z e. ( F " B ) ( ( F ` a ) u. ( F ` b ) ) C_ z ) )
70 69 ralima 
 |-  ( ( F Fn ~P A /\ B C_ ~P A ) -> ( A. y e. ( F " B ) E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z <-> A. b e. B E. z e. ( F " B ) ( ( F ` a ) u. ( F ` b ) ) C_ z ) )
71 1 4 70 syl2anc 
 |-  ( ph -> ( A. y e. ( F " B ) E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z <-> A. b e. B E. z e. ( F " B ) ( ( F ` a ) u. ( F ` b ) ) C_ z ) )
72 sseq2 
 |-  ( z = ( F ` c ) -> ( ( ( F ` a ) u. ( F ` b ) ) C_ z <-> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
73 72 rexima 
 |-  ( ( F Fn ~P A /\ B C_ ~P A ) -> ( E. z e. ( F " B ) ( ( F ` a ) u. ( F ` b ) ) C_ z <-> E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
74 1 4 73 syl2anc 
 |-  ( ph -> ( E. z e. ( F " B ) ( ( F ` a ) u. ( F ` b ) ) C_ z <-> E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
75 74 ralbidv 
 |-  ( ph -> ( A. b e. B E. z e. ( F " B ) ( ( F ` a ) u. ( F ` b ) ) C_ z <-> A. b e. B E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
76 71 75 bitrd 
 |-  ( ph -> ( A. y e. ( F " B ) E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z <-> A. b e. B E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
77 76 ralbidv 
 |-  ( ph -> ( A. a e. B A. y e. ( F " B ) E. z e. ( F " B ) ( ( F ` a ) u. y ) C_ z <-> A. a e. B A. b e. B E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
78 66 77 bitrd 
 |-  ( ph -> ( A. x e. ( F " B ) A. y e. ( F " B ) E. z e. ( F " B ) ( x u. y ) C_ z <-> A. a e. B A. b e. B E. c e. B ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
79 60 78 mpbird 
 |-  ( ph -> A. x e. ( F " B ) A. y e. ( F " B ) E. z e. ( F " B ) ( x u. y ) C_ z )
80 isipodrs 
 |-  ( ( toInc ` ( F " B ) ) e. Dirset <-> ( ( F " B ) e. _V /\ ( F " B ) =/= (/) /\ A. x e. ( F " B ) A. y e. ( F " B ) E. z e. ( F " B ) ( x u. y ) C_ z ) )
81 6 13 79 80 syl3anbrc 
 |-  ( ph -> ( toInc ` ( F " B ) ) e. Dirset )