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 ffvelrnd
 |-  ( ( 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 suceloni
 |-  ( ( `' 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 ) )