This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ttukeylem7

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1 
|- ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
ttukeylem.2 
|- ( ph -> B e. A )
ttukeylem.3 
|- ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
ttukeylem.4 
|- G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) )
Assertion ttukeylem7 
|- ( ph -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) )

Proof

Step Hyp Ref Expression
1 ttukeylem.1 
 |-  ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
2 ttukeylem.2 
 |-  ( ph -> B e. A )
3 ttukeylem.3 
 |-  ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
4 ttukeylem.4 
 |-  G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) )
5 fvex 
 |-  ( card ` ( U. A \ B ) ) e. _V
6 5 sucid 
 |-  ( card ` ( U. A \ B ) ) e. suc ( card ` ( U. A \ B ) )
7 1 2 3 4 ttukeylem6 
 |-  ( ( ph /\ ( card ` ( U. A \ B ) ) e. suc ( card ` ( U. A \ B ) ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) e. A )
8 6 7 mpan2 
 |-  ( ph -> ( G ` ( card ` ( U. A \ B ) ) ) e. A )
9 1 2 3 4 ttukeylem4 
 |-  ( ph -> ( G ` (/) ) = B )
10 0elon 
 |-  (/) e. On
11 cardon 
 |-  ( card ` ( U. A \ B ) ) e. On
12 0ss 
 |-  (/) C_ ( card ` ( U. A \ B ) )
13 10 11 12 3pm3.2i 
 |-  ( (/) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ (/) C_ ( card ` ( U. A \ B ) ) )
14 1 2 3 4 ttukeylem5 
 |-  ( ( ph /\ ( (/) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ (/) C_ ( card ` ( U. A \ B ) ) ) ) -> ( G ` (/) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
15 13 14 mpan2 
 |-  ( ph -> ( G ` (/) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
16 9 15 eqsstrrd 
 |-  ( ph -> B C_ ( G ` ( card ` ( U. A \ B ) ) ) )
17 simprr 
 |-  ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) C_ y )
18 ssun1 
 |-  y C_ ( y u. B )
19 undif1 
 |-  ( ( y \ B ) u. B ) = ( y u. B )
20 18 19 sseqtrri 
 |-  y C_ ( ( y \ B ) u. B )
21 simpl 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ph )
22 f1ocnv 
 |-  ( F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) -> `' F : ( U. A \ B ) -1-1-onto-> ( card ` ( U. A \ B ) ) )
23 f1of 
 |-  ( `' F : ( U. A \ B ) -1-1-onto-> ( card ` ( U. A \ B ) ) -> `' F : ( U. A \ B ) --> ( card ` ( U. A \ B ) ) )
24 1 22 23 3syl 
 |-  ( ph -> `' F : ( U. A \ B ) --> ( card ` ( U. A \ B ) ) )
25 24 adantr 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> `' F : ( U. A \ B ) --> ( card ` ( U. A \ B ) ) )
26 eldifi 
 |-  ( a e. ( y \ B ) -> a e. y )
27 26 ad2antll 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. y )
28 simprll 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> y e. A )
29 elunii 
 |-  ( ( a e. y /\ y e. A ) -> a e. U. A )
30 27 28 29 syl2anc 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. U. A )
31 eldifn 
 |-  ( a e. ( y \ B ) -> -. a e. B )
32 31 ad2antll 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> -. a e. B )
33 30 32 eldifd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( U. A \ B ) )
34 25 33 ffvelcdmd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) e. ( card ` ( U. A \ B ) ) )
35 onelon 
 |-  ( ( ( card ` ( U. A \ B ) ) e. On /\ ( `' F ` a ) e. ( card ` ( U. A \ B ) ) ) -> ( `' F ` a ) e. On )
36 11 34 35 sylancr 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) e. On )
37 onsuc 
 |-  ( ( `' F ` a ) e. On -> suc ( `' F ` a ) e. On )
38 36 37 syl 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) e. On )
39 11 a1i 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( card ` ( U. A \ B ) ) e. On )
40 11 onordi 
 |-  Ord ( card ` ( U. A \ B ) )
41 ordsucss 
 |-  ( Ord ( card ` ( U. A \ B ) ) -> ( ( `' F ` a ) e. ( card ` ( U. A \ B ) ) -> suc ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) )
42 40 34 41 mpsyl 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) )
43 1 2 3 4 ttukeylem5 
 |-  ( ( ph /\ ( suc ( `' F ` a ) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ suc ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) ) -> ( G ` suc ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
44 21 38 39 42 43 syl13anc 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` suc ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
45 ssun2 
 |-  if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) C_ ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) )
46 eloni 
 |-  ( ( `' F ` a ) e. On -> Ord ( `' F ` a ) )
47 ordunisuc 
 |-  ( Ord ( `' F ` a ) -> U. suc ( `' F ` a ) = ( `' F ` a ) )
48 36 46 47 3syl 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> U. suc ( `' F ` a ) = ( `' F ` a ) )
49 48 fveq2d 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( F ` U. suc ( `' F ` a ) ) = ( F ` ( `' F ` a ) ) )
50 1 adantr 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
51 f1ocnvfv2 
 |-  ( ( F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) /\ a e. ( U. A \ B ) ) -> ( F ` ( `' F ` a ) ) = a )
52 50 33 51 syl2anc 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( F ` ( `' F ` a ) ) = a )
53 49 52 eqtr2d 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a = ( F ` U. suc ( `' F ` a ) ) )
54 velsn 
 |-  ( a e. { ( F ` U. suc ( `' F ` a ) ) } <-> a = ( F ` U. suc ( `' F ` a ) ) )
55 53 54 sylibr 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. { ( F ` U. suc ( `' F ` a ) ) } )
56 48 fveq2d 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` U. suc ( `' F ` a ) ) = ( G ` ( `' F ` a ) ) )
57 ordelss 
 |-  ( ( Ord ( card ` ( U. A \ B ) ) /\ ( `' F ` a ) e. ( card ` ( U. A \ B ) ) ) -> ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) )
58 40 34 57 sylancr 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) )
59 1 2 3 4 ttukeylem5 
 |-  ( ( ph /\ ( ( `' F ` a ) e. On /\ ( card ` ( U. A \ B ) ) e. On /\ ( `' F ` a ) C_ ( card ` ( U. A \ B ) ) ) ) -> ( G ` ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
60 21 36 39 58 59 syl13anc 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
61 56 60 eqsstrd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` U. suc ( `' F ` a ) ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
62 simprlr 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) C_ y )
63 61 62 sstrd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` U. suc ( `' F ` a ) ) C_ y )
64 53 27 eqeltrrd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( F ` U. suc ( `' F ` a ) ) e. y )
65 64 snssd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> { ( F ` U. suc ( `' F ` a ) ) } C_ y )
66 63 65 unssd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) C_ y )
67 1 2 3 ttukeylem2 
 |-  ( ( ph /\ ( y e. A /\ ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) C_ y ) ) -> ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A )
68 21 28 66 67 syl12anc 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A )
69 68 iftrued 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) = { ( F ` U. suc ( `' F ` a ) ) } )
70 55 69 eleqtrrd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) )
71 45 70 sselid 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) )
72 1 2 3 4 ttukeylem3 
 |-  ( ( ph /\ suc ( `' F ` a ) e. On ) -> ( G ` suc ( `' F ` a ) ) = if ( suc ( `' F ` a ) = U. suc ( `' F ` a ) , if ( suc ( `' F ` a ) = (/) , B , U. ( G " suc ( `' F ` a ) ) ) , ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) )
73 38 72 syldan 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` suc ( `' F ` a ) ) = if ( suc ( `' F ` a ) = U. suc ( `' F ` a ) , if ( suc ( `' F ` a ) = (/) , B , U. ( G " suc ( `' F ` a ) ) ) , ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) )
74 sucidg 
 |-  ( ( `' F ` a ) e. ( card ` ( U. A \ B ) ) -> ( `' F ` a ) e. suc ( `' F ` a ) )
75 34 74 syl 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( `' F ` a ) e. suc ( `' F ` a ) )
76 ordirr 
 |-  ( Ord ( `' F ` a ) -> -. ( `' F ` a ) e. ( `' F ` a ) )
77 36 46 76 3syl 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> -. ( `' F ` a ) e. ( `' F ` a ) )
78 nelne1 
 |-  ( ( ( `' F ` a ) e. suc ( `' F ` a ) /\ -. ( `' F ` a ) e. ( `' F ` a ) ) -> suc ( `' F ` a ) =/= ( `' F ` a ) )
79 75 77 78 syl2anc 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) =/= ( `' F ` a ) )
80 79 48 neeqtrrd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> suc ( `' F ` a ) =/= U. suc ( `' F ` a ) )
81 80 neneqd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> -. suc ( `' F ` a ) = U. suc ( `' F ` a ) )
82 81 iffalsed 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> if ( suc ( `' F ` a ) = U. suc ( `' F ` a ) , if ( suc ( `' F ` a ) = (/) , B , U. ( G " suc ( `' F ` a ) ) ) , ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) ) = ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) )
83 73 82 eqtrd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> ( G ` suc ( `' F ` a ) ) = ( ( G ` U. suc ( `' F ` a ) ) u. if ( ( ( G ` U. suc ( `' F ` a ) ) u. { ( F ` U. suc ( `' F ` a ) ) } ) e. A , { ( F ` U. suc ( `' F ` a ) ) } , (/) ) ) )
84 71 83 eleqtrrd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( G ` suc ( `' F ` a ) ) )
85 44 84 sseldd 
 |-  ( ( ph /\ ( ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) /\ a e. ( y \ B ) ) ) -> a e. ( G ` ( card ` ( U. A \ B ) ) ) )
86 85 expr 
 |-  ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( a e. ( y \ B ) -> a e. ( G ` ( card ` ( U. A \ B ) ) ) ) )
87 86 ssrdv 
 |-  ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( y \ B ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
88 16 adantr 
 |-  ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> B C_ ( G ` ( card ` ( U. A \ B ) ) ) )
89 87 88 unssd 
 |-  ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( ( y \ B ) u. B ) C_ ( G ` ( card ` ( U. A \ B ) ) ) )
90 20 89 sstrid 
 |-  ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> y C_ ( G ` ( card ` ( U. A \ B ) ) ) )
91 17 90 eqssd 
 |-  ( ( ph /\ ( y e. A /\ ( G ` ( card ` ( U. A \ B ) ) ) C_ y ) ) -> ( G ` ( card ` ( U. A \ B ) ) ) = y )
92 91 expr 
 |-  ( ( ph /\ y e. A ) -> ( ( G ` ( card ` ( U. A \ B ) ) ) C_ y -> ( G ` ( card ` ( U. A \ B ) ) ) = y ) )
93 npss 
 |-  ( -. ( G ` ( card ` ( U. A \ B ) ) ) C. y <-> ( ( G ` ( card ` ( U. A \ B ) ) ) C_ y -> ( G ` ( card ` ( U. A \ B ) ) ) = y ) )
94 92 93 sylibr 
 |-  ( ( ph /\ y e. A ) -> -. ( G ` ( card ` ( U. A \ B ) ) ) C. y )
95 94 ralrimiva 
 |-  ( ph -> A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y )
96 sseq2 
 |-  ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( B C_ x <-> B C_ ( G ` ( card ` ( U. A \ B ) ) ) ) )
97 psseq1 
 |-  ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( x C. y <-> ( G ` ( card ` ( U. A \ B ) ) ) C. y ) )
98 97 notbid 
 |-  ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( -. x C. y <-> -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) )
99 98 ralbidv 
 |-  ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( A. y e. A -. x C. y <-> A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) )
100 96 99 anbi12d 
 |-  ( x = ( G ` ( card ` ( U. A \ B ) ) ) -> ( ( B C_ x /\ A. y e. A -. x C. y ) <-> ( B C_ ( G ` ( card ` ( U. A \ B ) ) ) /\ A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) ) )
101 100 rspcev 
 |-  ( ( ( G ` ( card ` ( U. A \ B ) ) ) e. A /\ ( B C_ ( G ` ( card ` ( U. A \ B ) ) ) /\ A. y e. A -. ( G ` ( card ` ( U. A \ B ) ) ) C. y ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) )
102 8 16 95 101 syl12anc 
 |-  ( ph -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) )