Metamath Proof Explorer


Theorem erdszelem8

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze.n
|- ( ph -> N e. NN )
erdsze.f
|- ( ph -> F : ( 1 ... N ) -1-1-> RR )
erdszelem.k
|- K = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
erdszelem.o
|- O Or RR
erdszelem.a
|- ( ph -> A e. ( 1 ... N ) )
erdszelem.b
|- ( ph -> B e. ( 1 ... N ) )
erdszelem.l
|- ( ph -> A < B )
Assertion erdszelem8
|- ( ph -> ( ( K ` A ) = ( K ` B ) -> -. ( F ` A ) O ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 erdsze.n
 |-  ( ph -> N e. NN )
2 erdsze.f
 |-  ( ph -> F : ( 1 ... N ) -1-1-> RR )
3 erdszelem.k
 |-  K = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
4 erdszelem.o
 |-  O Or RR
5 erdszelem.a
 |-  ( ph -> A e. ( 1 ... N ) )
6 erdszelem.b
 |-  ( ph -> B e. ( 1 ... N ) )
7 erdszelem.l
 |-  ( ph -> A < B )
8 hashf
 |-  # : _V --> ( NN0 u. { +oo } )
9 ffun
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> Fun # )
10 8 9 ax-mp
 |-  Fun #
11 1 2 3 4 erdszelem5
 |-  ( ( ph /\ A e. ( 1 ... N ) ) -> ( K ` A ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
12 5 11 mpdan
 |-  ( ph -> ( K ` A ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) )
13 fvelima
 |-  ( ( Fun # /\ ( K ` A ) e. ( # " { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) ) -> E. f e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ( # ` f ) = ( K ` A ) )
14 10 12 13 sylancr
 |-  ( ph -> E. f e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ( # ` f ) = ( K ` A ) )
15 eqid
 |-  { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) }
16 15 erdszelem1
 |-  ( f e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } <-> ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) )
17 fzfid
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( 1 ... A ) e. Fin )
18 simplr1
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> f C_ ( 1 ... A ) )
19 ssfi
 |-  ( ( ( 1 ... A ) e. Fin /\ f C_ ( 1 ... A ) ) -> f e. Fin )
20 17 18 19 syl2anc
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> f e. Fin )
21 hashcl
 |-  ( f e. Fin -> ( # ` f ) e. NN0 )
22 20 21 syl
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # ` f ) e. NN0 )
23 22 nn0red
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # ` f ) e. RR )
24 eqid
 |-  { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } = { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) }
25 24 erdszelem2
 |-  ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) e. Fin /\ ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) C_ NN )
26 25 simpri
 |-  ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) C_ NN
27 nnssre
 |-  NN C_ RR
28 26 27 sstri
 |-  ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) C_ RR
29 28 a1i
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) C_ RR )
30 5 elfzelzd
 |-  ( ph -> A e. ZZ )
31 6 elfzelzd
 |-  ( ph -> B e. ZZ )
32 elfznn
 |-  ( A e. ( 1 ... N ) -> A e. NN )
33 5 32 syl
 |-  ( ph -> A e. NN )
34 33 nnred
 |-  ( ph -> A e. RR )
35 elfznn
 |-  ( B e. ( 1 ... N ) -> B e. NN )
36 6 35 syl
 |-  ( ph -> B e. NN )
37 36 nnred
 |-  ( ph -> B e. RR )
38 34 37 7 ltled
 |-  ( ph -> A <_ B )
39 eluz2
 |-  ( B e. ( ZZ>= ` A ) <-> ( A e. ZZ /\ B e. ZZ /\ A <_ B ) )
40 30 31 38 39 syl3anbrc
 |-  ( ph -> B e. ( ZZ>= ` A ) )
41 fzss2
 |-  ( B e. ( ZZ>= ` A ) -> ( 1 ... A ) C_ ( 1 ... B ) )
42 40 41 syl
 |-  ( ph -> ( 1 ... A ) C_ ( 1 ... B ) )
43 42 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( 1 ... A ) C_ ( 1 ... B ) )
44 18 43 sstrd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> f C_ ( 1 ... B ) )
45 elfz1end
 |-  ( B e. NN <-> B e. ( 1 ... B ) )
46 36 45 sylib
 |-  ( ph -> B e. ( 1 ... B ) )
47 46 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> B e. ( 1 ... B ) )
48 47 snssd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> { B } C_ ( 1 ... B ) )
49 44 48 unssd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( f u. { B } ) C_ ( 1 ... B ) )
50 simplr2
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( F |` f ) Isom < , O ( f , ( F " f ) ) )
51 f1f
 |-  ( F : ( 1 ... N ) -1-1-> RR -> F : ( 1 ... N ) --> RR )
52 2 51 syl
 |-  ( ph -> F : ( 1 ... N ) --> RR )
53 52 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> F : ( 1 ... N ) --> RR )
54 elfzuz3
 |-  ( A e. ( 1 ... N ) -> N e. ( ZZ>= ` A ) )
55 fzss2
 |-  ( N e. ( ZZ>= ` A ) -> ( 1 ... A ) C_ ( 1 ... N ) )
56 5 54 55 3syl
 |-  ( ph -> ( 1 ... A ) C_ ( 1 ... N ) )
57 56 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( 1 ... A ) C_ ( 1 ... N ) )
58 18 57 sstrd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> f C_ ( 1 ... N ) )
59 fzssuz
 |-  ( 1 ... N ) C_ ( ZZ>= ` 1 )
60 uzssz
 |-  ( ZZ>= ` 1 ) C_ ZZ
61 zssre
 |-  ZZ C_ RR
62 60 61 sstri
 |-  ( ZZ>= ` 1 ) C_ RR
63 59 62 sstri
 |-  ( 1 ... N ) C_ RR
64 ltso
 |-  < Or RR
65 soss
 |-  ( ( 1 ... N ) C_ RR -> ( < Or RR -> < Or ( 1 ... N ) ) )
66 63 64 65 mp2
 |-  < Or ( 1 ... N )
67 soisores
 |-  ( ( ( < Or ( 1 ... N ) /\ O Or RR ) /\ ( F : ( 1 ... N ) --> RR /\ f C_ ( 1 ... N ) ) ) -> ( ( F |` f ) Isom < , O ( f , ( F " f ) ) <-> A. z e. f A. w e. f ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
68 66 4 67 mpanl12
 |-  ( ( F : ( 1 ... N ) --> RR /\ f C_ ( 1 ... N ) ) -> ( ( F |` f ) Isom < , O ( f , ( F " f ) ) <-> A. z e. f A. w e. f ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
69 53 58 68 syl2anc
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( ( F |` f ) Isom < , O ( f , ( F " f ) ) <-> A. z e. f A. w e. f ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
70 50 69 mpbid
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> A. z e. f A. w e. f ( z < w -> ( F ` z ) O ( F ` w ) ) )
71 70 r19.21bi
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> A. w e. f ( z < w -> ( F ` z ) O ( F ` w ) ) )
72 18 sselda
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> z e. ( 1 ... A ) )
73 elfzle2
 |-  ( z e. ( 1 ... A ) -> z <_ A )
74 72 73 syl
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> z <_ A )
75 58 sselda
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> z e. ( 1 ... N ) )
76 63 75 sseldi
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> z e. RR )
77 5 ad3antrrr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> A e. ( 1 ... N ) )
78 77 32 syl
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> A e. NN )
79 78 nnred
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> A e. RR )
80 76 79 lenltd
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( z <_ A <-> -. A < z ) )
81 74 80 mpbid
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> -. A < z )
82 50 adantr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( F |` f ) Isom < , O ( f , ( F " f ) ) )
83 simplr3
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> A e. f )
84 83 adantr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> A e. f )
85 simpr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> z e. f )
86 isorel
 |-  ( ( ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ ( A e. f /\ z e. f ) ) -> ( A < z <-> ( ( F |` f ) ` A ) O ( ( F |` f ) ` z ) ) )
87 fvres
 |-  ( A e. f -> ( ( F |` f ) ` A ) = ( F ` A ) )
88 fvres
 |-  ( z e. f -> ( ( F |` f ) ` z ) = ( F ` z ) )
89 87 88 breqan12d
 |-  ( ( A e. f /\ z e. f ) -> ( ( ( F |` f ) ` A ) O ( ( F |` f ) ` z ) <-> ( F ` A ) O ( F ` z ) ) )
90 89 adantl
 |-  ( ( ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ ( A e. f /\ z e. f ) ) -> ( ( ( F |` f ) ` A ) O ( ( F |` f ) ` z ) <-> ( F ` A ) O ( F ` z ) ) )
91 86 90 bitrd
 |-  ( ( ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ ( A e. f /\ z e. f ) ) -> ( A < z <-> ( F ` A ) O ( F ` z ) ) )
92 82 84 85 91 syl12anc
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( A < z <-> ( F ` A ) O ( F ` z ) ) )
93 81 92 mtbid
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> -. ( F ` A ) O ( F ` z ) )
94 simplr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( F ` A ) O ( F ` B ) )
95 53 adantr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> F : ( 1 ... N ) --> RR )
96 95 75 ffvelrnd
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( F ` z ) e. RR )
97 95 77 ffvelrnd
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( F ` A ) e. RR )
98 6 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> B e. ( 1 ... N ) )
99 98 adantr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> B e. ( 1 ... N ) )
100 95 99 ffvelrnd
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( F ` B ) e. RR )
101 sotr2
 |-  ( ( O Or RR /\ ( ( F ` z ) e. RR /\ ( F ` A ) e. RR /\ ( F ` B ) e. RR ) ) -> ( ( -. ( F ` A ) O ( F ` z ) /\ ( F ` A ) O ( F ` B ) ) -> ( F ` z ) O ( F ` B ) ) )
102 4 101 mpan
 |-  ( ( ( F ` z ) e. RR /\ ( F ` A ) e. RR /\ ( F ` B ) e. RR ) -> ( ( -. ( F ` A ) O ( F ` z ) /\ ( F ` A ) O ( F ` B ) ) -> ( F ` z ) O ( F ` B ) ) )
103 96 97 100 102 syl3anc
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( ( -. ( F ` A ) O ( F ` z ) /\ ( F ` A ) O ( F ` B ) ) -> ( F ` z ) O ( F ` B ) ) )
104 93 94 103 mp2and
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( F ` z ) O ( F ` B ) )
105 104 a1d
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( z < w -> ( F ` z ) O ( F ` B ) ) )
106 elsni
 |-  ( w e. { B } -> w = B )
107 106 fveq2d
 |-  ( w e. { B } -> ( F ` w ) = ( F ` B ) )
108 107 breq2d
 |-  ( w e. { B } -> ( ( F ` z ) O ( F ` w ) <-> ( F ` z ) O ( F ` B ) ) )
109 108 imbi2d
 |-  ( w e. { B } -> ( ( z < w -> ( F ` z ) O ( F ` w ) ) <-> ( z < w -> ( F ` z ) O ( F ` B ) ) ) )
110 105 109 syl5ibrcom
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> ( w e. { B } -> ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
111 110 ralrimiv
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> A. w e. { B } ( z < w -> ( F ` z ) O ( F ` w ) ) )
112 ralunb
 |-  ( A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) <-> ( A. w e. f ( z < w -> ( F ` z ) O ( F ` w ) ) /\ A. w e. { B } ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
113 71 111 112 sylanbrc
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ z e. f ) -> A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) )
114 113 ralrimiva
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> A. z e. f A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) )
115 49 sselda
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( f u. { B } ) ) -> w e. ( 1 ... B ) )
116 elfzle2
 |-  ( w e. ( 1 ... B ) -> w <_ B )
117 116 adantl
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( 1 ... B ) ) -> w <_ B )
118 elfzelz
 |-  ( w e. ( 1 ... B ) -> w e. ZZ )
119 118 zred
 |-  ( w e. ( 1 ... B ) -> w e. RR )
120 119 adantl
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( 1 ... B ) ) -> w e. RR )
121 37 ad3antrrr
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( 1 ... B ) ) -> B e. RR )
122 120 121 lenltd
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( 1 ... B ) ) -> ( w <_ B <-> -. B < w ) )
123 117 122 mpbid
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( 1 ... B ) ) -> -. B < w )
124 115 123 syldan
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( f u. { B } ) ) -> -. B < w )
125 124 pm2.21d
 |-  ( ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) /\ w e. ( f u. { B } ) ) -> ( B < w -> ( F ` z ) O ( F ` w ) ) )
126 125 ralrimiva
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> A. w e. ( f u. { B } ) ( B < w -> ( F ` z ) O ( F ` w ) ) )
127 elsni
 |-  ( z e. { B } -> z = B )
128 127 breq1d
 |-  ( z e. { B } -> ( z < w <-> B < w ) )
129 128 imbi1d
 |-  ( z e. { B } -> ( ( z < w -> ( F ` z ) O ( F ` w ) ) <-> ( B < w -> ( F ` z ) O ( F ` w ) ) ) )
130 129 ralbidv
 |-  ( z e. { B } -> ( A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) <-> A. w e. ( f u. { B } ) ( B < w -> ( F ` z ) O ( F ` w ) ) ) )
131 126 130 syl5ibrcom
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( z e. { B } -> A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
132 131 ralrimiv
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> A. z e. { B } A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) )
133 ralunb
 |-  ( A. z e. ( f u. { B } ) A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) <-> ( A. z e. f A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) /\ A. z e. { B } A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
134 114 132 133 sylanbrc
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> A. z e. ( f u. { B } ) A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) )
135 98 snssd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> { B } C_ ( 1 ... N ) )
136 58 135 unssd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( f u. { B } ) C_ ( 1 ... N ) )
137 soisores
 |-  ( ( ( < Or ( 1 ... N ) /\ O Or RR ) /\ ( F : ( 1 ... N ) --> RR /\ ( f u. { B } ) C_ ( 1 ... N ) ) ) -> ( ( F |` ( f u. { B } ) ) Isom < , O ( ( f u. { B } ) , ( F " ( f u. { B } ) ) ) <-> A. z e. ( f u. { B } ) A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
138 66 4 137 mpanl12
 |-  ( ( F : ( 1 ... N ) --> RR /\ ( f u. { B } ) C_ ( 1 ... N ) ) -> ( ( F |` ( f u. { B } ) ) Isom < , O ( ( f u. { B } ) , ( F " ( f u. { B } ) ) ) <-> A. z e. ( f u. { B } ) A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
139 53 136 138 syl2anc
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( ( F |` ( f u. { B } ) ) Isom < , O ( ( f u. { B } ) , ( F " ( f u. { B } ) ) ) <-> A. z e. ( f u. { B } ) A. w e. ( f u. { B } ) ( z < w -> ( F ` z ) O ( F ` w ) ) ) )
140 134 139 mpbird
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( F |` ( f u. { B } ) ) Isom < , O ( ( f u. { B } ) , ( F " ( f u. { B } ) ) ) )
141 ssun2
 |-  { B } C_ ( f u. { B } )
142 snssg
 |-  ( B e. ( 1 ... B ) -> ( B e. ( f u. { B } ) <-> { B } C_ ( f u. { B } ) ) )
143 47 142 syl
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( B e. ( f u. { B } ) <-> { B } C_ ( f u. { B } ) ) )
144 141 143 mpbiri
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> B e. ( f u. { B } ) )
145 24 erdszelem1
 |-  ( ( f u. { B } ) e. { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } <-> ( ( f u. { B } ) C_ ( 1 ... B ) /\ ( F |` ( f u. { B } ) ) Isom < , O ( ( f u. { B } ) , ( F " ( f u. { B } ) ) ) /\ B e. ( f u. { B } ) ) )
146 49 140 144 145 syl3anbrc
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( f u. { B } ) e. { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } )
147 vex
 |-  f e. _V
148 snex
 |-  { B } e. _V
149 147 148 unex
 |-  ( f u. { B } ) e. _V
150 8 fdmi
 |-  dom # = _V
151 149 150 eleqtrri
 |-  ( f u. { B } ) e. dom #
152 funfvima
 |-  ( ( Fun # /\ ( f u. { B } ) e. dom # ) -> ( ( f u. { B } ) e. { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } -> ( # ` ( f u. { B } ) ) e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) ) )
153 10 151 152 mp2an
 |-  ( ( f u. { B } ) e. { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } -> ( # ` ( f u. { B } ) ) e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) )
154 146 153 syl
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # ` ( f u. { B } ) ) e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) )
155 154 ne0d
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) =/= (/) )
156 25 simpli
 |-  ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) e. Fin
157 fimaxre2
 |-  ( ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) C_ RR /\ ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) e. Fin ) -> E. z e. RR A. w e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) w <_ z )
158 29 156 157 sylancl
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> E. z e. RR A. w e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) w <_ z )
159 34 37 ltnled
 |-  ( ph -> ( A < B <-> -. B <_ A ) )
160 7 159 mpbid
 |-  ( ph -> -. B <_ A )
161 elfzle2
 |-  ( B e. ( 1 ... A ) -> B <_ A )
162 160 161 nsyl
 |-  ( ph -> -. B e. ( 1 ... A ) )
163 162 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> -. B e. ( 1 ... A ) )
164 18 163 ssneldd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> -. B e. f )
165 hashunsng
 |-  ( B e. ( 1 ... N ) -> ( ( f e. Fin /\ -. B e. f ) -> ( # ` ( f u. { B } ) ) = ( ( # ` f ) + 1 ) ) )
166 98 165 syl
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( ( f e. Fin /\ -. B e. f ) -> ( # ` ( f u. { B } ) ) = ( ( # ` f ) + 1 ) ) )
167 20 164 166 mp2and
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # ` ( f u. { B } ) ) = ( ( # ` f ) + 1 ) )
168 167 154 eqeltrrd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( ( # ` f ) + 1 ) e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) )
169 suprub
 |-  ( ( ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) C_ RR /\ ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) =/= (/) /\ E. z e. RR A. w e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) w <_ z ) /\ ( ( # ` f ) + 1 ) e. ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) ) -> ( ( # ` f ) + 1 ) <_ sup ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) , RR , < ) )
170 29 155 158 168 169 syl31anc
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( ( # ` f ) + 1 ) <_ sup ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) , RR , < ) )
171 1 2 3 erdszelem3
 |-  ( B e. ( 1 ... N ) -> ( K ` B ) = sup ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) , RR , < ) )
172 6 171 syl
 |-  ( ph -> ( K ` B ) = sup ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) , RR , < ) )
173 172 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( K ` B ) = sup ( ( # " { y e. ~P ( 1 ... B ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ B e. y ) } ) , RR , < ) )
174 170 173 breqtrrd
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( ( # ` f ) + 1 ) <_ ( K ` B ) )
175 1 2 3 4 erdszelem6
 |-  ( ph -> K : ( 1 ... N ) --> NN )
176 175 6 ffvelrnd
 |-  ( ph -> ( K ` B ) e. NN )
177 176 ad2antrr
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( K ` B ) e. NN )
178 177 nnnn0d
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( K ` B ) e. NN0 )
179 nn0ltp1le
 |-  ( ( ( # ` f ) e. NN0 /\ ( K ` B ) e. NN0 ) -> ( ( # ` f ) < ( K ` B ) <-> ( ( # ` f ) + 1 ) <_ ( K ` B ) ) )
180 22 178 179 syl2anc
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( ( # ` f ) < ( K ` B ) <-> ( ( # ` f ) + 1 ) <_ ( K ` B ) ) )
181 174 180 mpbird
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # ` f ) < ( K ` B ) )
182 23 181 ltned
 |-  ( ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) /\ ( F ` A ) O ( F ` B ) ) -> ( # ` f ) =/= ( K ` B ) )
183 182 ex
 |-  ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) -> ( ( F ` A ) O ( F ` B ) -> ( # ` f ) =/= ( K ` B ) ) )
184 neeq1
 |-  ( ( # ` f ) = ( K ` A ) -> ( ( # ` f ) =/= ( K ` B ) <-> ( K ` A ) =/= ( K ` B ) ) )
185 184 imbi2d
 |-  ( ( # ` f ) = ( K ` A ) -> ( ( ( F ` A ) O ( F ` B ) -> ( # ` f ) =/= ( K ` B ) ) <-> ( ( F ` A ) O ( F ` B ) -> ( K ` A ) =/= ( K ` B ) ) ) )
186 183 185 syl5ibcom
 |-  ( ( ph /\ ( f C_ ( 1 ... A ) /\ ( F |` f ) Isom < , O ( f , ( F " f ) ) /\ A e. f ) ) -> ( ( # ` f ) = ( K ` A ) -> ( ( F ` A ) O ( F ` B ) -> ( K ` A ) =/= ( K ` B ) ) ) )
187 16 186 sylan2b
 |-  ( ( ph /\ f e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) -> ( ( # ` f ) = ( K ` A ) -> ( ( F ` A ) O ( F ` B ) -> ( K ` A ) =/= ( K ` B ) ) ) )
188 187 rexlimdva
 |-  ( ph -> ( E. f e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ( # ` f ) = ( K ` A ) -> ( ( F ` A ) O ( F ` B ) -> ( K ` A ) =/= ( K ` B ) ) ) )
189 14 188 mpd
 |-  ( ph -> ( ( F ` A ) O ( F ` B ) -> ( K ` A ) =/= ( K ` B ) ) )
190 189 necon2bd
 |-  ( ph -> ( ( K ` A ) = ( K ` B ) -> -. ( F ` A ) O ( F ` B ) ) )