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 sselid 
 |-  ( ( ( ( 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 ) ) )