Metamath Proof Explorer

Theorem ismrcd2

Description: Second half of ismrcd1 . (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses ismrcd.b 
|- ( ph -> B e. V )
ismrcd.f 
|- ( ph -> F : ~P B --> ~P B )
ismrcd.e 
|- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
ismrcd.m 
|- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )
ismrcd.i 
|- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )
Assertion ismrcd2 
|- ( ph -> F = ( mrCls ` dom ( F i^i _I ) ) )

Proof

Step Hyp Ref Expression
1 ismrcd.b 
 |-  ( ph -> B e. V )
2 ismrcd.f 
 |-  ( ph -> F : ~P B --> ~P B )
3 ismrcd.e 
 |-  ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
4 ismrcd.m 
 |-  ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )
5 ismrcd.i 
 |-  ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )
6 2 ffnd 
 |-  ( ph -> F Fn ~P B )
7 1 2 3 4 5 ismrcd1 
 |-  ( ph -> dom ( F i^i _I ) e. ( Moore ` B ) )
8 eqid 
 |-  ( mrCls ` dom ( F i^i _I ) ) = ( mrCls ` dom ( F i^i _I ) )
9 8 mrcf 
 |-  ( dom ( F i^i _I ) e. ( Moore ` B ) -> ( mrCls ` dom ( F i^i _I ) ) : ~P B --> dom ( F i^i _I ) )
10 ffn 
 |-  ( ( mrCls ` dom ( F i^i _I ) ) : ~P B --> dom ( F i^i _I ) -> ( mrCls ` dom ( F i^i _I ) ) Fn ~P B )
11 7 9 10 3syl 
 |-  ( ph -> ( mrCls ` dom ( F i^i _I ) ) Fn ~P B )
12 7 8 mrcssvd 
 |-  ( ph -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B )
13 12 adantr 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B )
14 elpwi 
 |-  ( z e. ~P B -> z C_ B )
15 8 mrcssid 
 |-  ( ( dom ( F i^i _I ) e. ( Moore ` B ) /\ z C_ B ) -> z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) )
16 7 14 15 syl2an 
 |-  ( ( ph /\ z e. ~P B ) -> z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) )
17 4 3expib 
 |-  ( ph -> ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
18 17 alrimivv 
 |-  ( ph -> A. y A. x ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
19 vex 
 |-  z e. _V
20 fvex 
 |-  ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. _V
21 sseq1 
 |-  ( x = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) -> ( x C_ B <-> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B ) )
22 21 adantl 
 |-  ( ( y = z /\ x = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( x C_ B <-> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B ) )
23 sseq12 
 |-  ( ( y = z /\ x = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( y C_ x <-> z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) )
24 22 23 anbi12d 
 |-  ( ( y = z /\ x = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( ( x C_ B /\ y C_ x ) <-> ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B /\ z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) )
25 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
26 fveq2 
 |-  ( x = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) -> ( F ` x ) = ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) )
27 sseq12 
 |-  ( ( ( F ` y ) = ( F ` z ) /\ ( F ` x ) = ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) -> ( ( F ` y ) C_ ( F ` x ) <-> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) )
28 25 26 27 syl2an 
 |-  ( ( y = z /\ x = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( ( F ` y ) C_ ( F ` x ) <-> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) )
29 24 28 imbi12d 
 |-  ( ( y = z /\ x = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) <-> ( ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B /\ z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) ) )
30 29 spc2gv 
 |-  ( ( z e. _V /\ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. _V ) -> ( A. y A. x ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) -> ( ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B /\ z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) ) )
31 19 20 30 mp2an 
 |-  ( A. y A. x ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) -> ( ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B /\ z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) )
32 18 31 syl 
 |-  ( ph -> ( ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B /\ z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) )
33 32 adantr 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B /\ z C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) -> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) ) )
34 13 16 33 mp2and 
 |-  ( ( ph /\ z e. ~P B ) -> ( F ` z ) C_ ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) )
35 8 mrccl 
 |-  ( ( dom ( F i^i _I ) e. ( Moore ` B ) /\ z C_ B ) -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. dom ( F i^i _I ) )
36 7 14 35 syl2an 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. dom ( F i^i _I ) )
37 6 adantr 
 |-  ( ( ph /\ z e. ~P B ) -> F Fn ~P B )
38 20 elpw 
 |-  ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. ~P B <-> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ B )
39 12 38 sylibr 
 |-  ( ph -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. ~P B )
40 39 adantr 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. ~P B )
41 fnelfp 
 |-  ( ( F Fn ~P B /\ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. ~P B ) -> ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. dom ( F i^i _I ) <-> ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) )
42 37 40 41 syl2anc 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( ( mrCls ` dom ( F i^i _I ) ) ` z ) e. dom ( F i^i _I ) <-> ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) )
43 36 42 mpbid 
 |-  ( ( ph /\ z e. ~P B ) -> ( F ` ( ( mrCls ` dom ( F i^i _I ) ) ` z ) ) = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) )
44 34 43 sseqtrd 
 |-  ( ( ph /\ z e. ~P B ) -> ( F ` z ) C_ ( ( mrCls ` dom ( F i^i _I ) ) ` z ) )
45 7 adantr 
 |-  ( ( ph /\ z e. ~P B ) -> dom ( F i^i _I ) e. ( Moore ` B ) )
46 sseq1 
 |-  ( x = z -> ( x C_ B <-> z C_ B ) )
47 46 anbi2d 
 |-  ( x = z -> ( ( ph /\ x C_ B ) <-> ( ph /\ z C_ B ) ) )
48 id 
 |-  ( x = z -> x = z )
49 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
50 48 49 sseq12d 
 |-  ( x = z -> ( x C_ ( F ` x ) <-> z C_ ( F ` z ) ) )
51 47 50 imbi12d 
 |-  ( x = z -> ( ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) ) <-> ( ( ph /\ z C_ B ) -> z C_ ( F ` z ) ) ) )
52 51 3 chvarvv 
 |-  ( ( ph /\ z C_ B ) -> z C_ ( F ` z ) )
53 14 52 sylan2 
 |-  ( ( ph /\ z e. ~P B ) -> z C_ ( F ` z ) )
54 2fveq3 
 |-  ( x = z -> ( F ` ( F ` x ) ) = ( F ` ( F ` z ) ) )
55 54 49 eqeq12d 
 |-  ( x = z -> ( ( F ` ( F ` x ) ) = ( F ` x ) <-> ( F ` ( F ` z ) ) = ( F ` z ) ) )
56 47 55 imbi12d 
 |-  ( x = z -> ( ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) ) <-> ( ( ph /\ z C_ B ) -> ( F ` ( F ` z ) ) = ( F ` z ) ) ) )
57 56 5 chvarvv 
 |-  ( ( ph /\ z C_ B ) -> ( F ` ( F ` z ) ) = ( F ` z ) )
58 14 57 sylan2 
 |-  ( ( ph /\ z e. ~P B ) -> ( F ` ( F ` z ) ) = ( F ` z ) )
59 2 ffvelcdmda 
 |-  ( ( ph /\ z e. ~P B ) -> ( F ` z ) e. ~P B )
60 fnelfp 
 |-  ( ( F Fn ~P B /\ ( F ` z ) e. ~P B ) -> ( ( F ` z ) e. dom ( F i^i _I ) <-> ( F ` ( F ` z ) ) = ( F ` z ) ) )
61 37 59 60 syl2anc 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( F ` z ) e. dom ( F i^i _I ) <-> ( F ` ( F ` z ) ) = ( F ` z ) ) )
62 58 61 mpbird 
 |-  ( ( ph /\ z e. ~P B ) -> ( F ` z ) e. dom ( F i^i _I ) )
63 8 mrcsscl 
 |-  ( ( dom ( F i^i _I ) e. ( Moore ` B ) /\ z C_ ( F ` z ) /\ ( F ` z ) e. dom ( F i^i _I ) ) -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ ( F ` z ) )
64 45 53 62 63 syl3anc 
 |-  ( ( ph /\ z e. ~P B ) -> ( ( mrCls ` dom ( F i^i _I ) ) ` z ) C_ ( F ` z ) )
65 44 64 eqssd 
 |-  ( ( ph /\ z e. ~P B ) -> ( F ` z ) = ( ( mrCls ` dom ( F i^i _I ) ) ` z ) )
66 6 11 65 eqfnfvd 
 |-  ( ph -> F = ( mrCls ` dom ( F i^i _I ) ) )