Metamath Proof Explorer

Theorem ttukey2g

Description: The Teichmüller-Tukey Lemma ttukey with a slightly stronger conclusion: we can set up the maximal element of A so that it also contains some given B e. A as a subset. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion ttukey2g 
|- ( ( U. A e. dom card /\ B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( U. A \ B ) C_ U. A
2 ssnum 
 |-  ( ( U. A e. dom card /\ ( U. A \ B ) C_ U. A ) -> ( U. A \ B ) e. dom card )
3 1 2 mpan2 
 |-  ( U. A e. dom card -> ( U. A \ B ) e. dom card )
4 isnum3 
 |-  ( ( U. A \ B ) e. dom card <-> ( card ` ( U. A \ B ) ) ~~ ( U. A \ B ) )
5 bren 
 |-  ( ( card ` ( U. A \ B ) ) ~~ ( U. A \ B ) <-> E. f f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
6 4 5 bitri 
 |-  ( ( U. A \ B ) e. dom card <-> E. f f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
7 simp1 
 |-  ( ( f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) /\ B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )
8 simp2 
 |-  ( ( f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) /\ B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> B e. A )
9 simp3 
 |-  ( ( f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) /\ B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )
10 dmeq 
 |-  ( w = z -> dom w = dom z )
11 10 unieqd 
 |-  ( w = z -> U. dom w = U. dom z )
12 10 11 eqeq12d 
 |-  ( w = z -> ( dom w = U. dom w <-> dom z = U. dom z ) )
13 10 eqeq1d 
 |-  ( w = z -> ( dom w = (/) <-> dom z = (/) ) )
14 rneq 
 |-  ( w = z -> ran w = ran z )
15 14 unieqd 
 |-  ( w = z -> U. ran w = U. ran z )
16 13 15 ifbieq2d 
 |-  ( w = z -> if ( dom w = (/) , B , U. ran w ) = if ( dom z = (/) , B , U. ran z ) )
17 id 
 |-  ( w = z -> w = z )
18 17 11 fveq12d 
 |-  ( w = z -> ( w ` U. dom w ) = ( z ` U. dom z ) )
19 11 fveq2d 
 |-  ( w = z -> ( f ` U. dom w ) = ( f ` U. dom z ) )
20 19 sneqd 
 |-  ( w = z -> { ( f ` U. dom w ) } = { ( f ` U. dom z ) } )
21 18 20 uneq12d 
 |-  ( w = z -> ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) = ( ( z ` U. dom z ) u. { ( f ` U. dom z ) } ) )
22 21 eleq1d 
 |-  ( w = z -> ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A <-> ( ( z ` U. dom z ) u. { ( f ` U. dom z ) } ) e. A ) )
23 22 20 ifbieq1d 
 |-  ( w = z -> if ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A , { ( f ` U. dom w ) } , (/) ) = if ( ( ( z ` U. dom z ) u. { ( f ` U. dom z ) } ) e. A , { ( f ` U. dom z ) } , (/) ) )
24 18 23 uneq12d 
 |-  ( w = z -> ( ( w ` U. dom w ) u. if ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A , { ( f ` U. dom w ) } , (/) ) ) = ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( f ` U. dom z ) } ) e. A , { ( f ` U. dom z ) } , (/) ) ) )
25 12 16 24 ifbieq12d 
 |-  ( w = z -> if ( dom w = U. dom w , if ( dom w = (/) , B , U. ran w ) , ( ( w ` U. dom w ) u. if ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A , { ( f ` U. dom w ) } , (/) ) ) ) = 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 ) } , (/) ) ) ) )
26 25 cbvmptv 
 |-  ( w e. _V |-> if ( dom w = U. dom w , if ( dom w = (/) , B , U. ran w ) , ( ( w ` U. dom w ) u. if ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A , { ( f ` U. dom w ) } , (/) ) ) ) ) = ( 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 ) } , (/) ) ) ) )
27 recseq 
 |-  ( ( w e. _V |-> if ( dom w = U. dom w , if ( dom w = (/) , B , U. ran w ) , ( ( w ` U. dom w ) u. if ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A , { ( f ` U. dom w ) } , (/) ) ) ) ) = ( 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 ) } , (/) ) ) ) ) -> recs ( ( w e. _V |-> if ( dom w = U. dom w , if ( dom w = (/) , B , U. ran w ) , ( ( w ` U. dom w ) u. if ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A , { ( f ` U. dom w ) } , (/) ) ) ) ) ) = 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 ) } , (/) ) ) ) ) ) )
28 26 27 ax-mp 
 |-  recs ( ( w e. _V |-> if ( dom w = U. dom w , if ( dom w = (/) , B , U. ran w ) , ( ( w ` U. dom w ) u. if ( ( ( w ` U. dom w ) u. { ( f ` U. dom w ) } ) e. A , { ( f ` U. dom w ) } , (/) ) ) ) ) ) = 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 ) } , (/) ) ) ) ) )
29 7 8 9 28 ttukeylem7 
 |-  ( ( f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) /\ B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) )
30 29 3expib 
 |-  ( f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) -> ( ( B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) ) )
31 30 exlimiv 
 |-  ( E. f f : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) -> ( ( B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) ) )
32 6 31 sylbi 
 |-  ( ( U. A \ B ) e. dom card -> ( ( B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) ) )
33 3 32 syl 
 |-  ( U. A e. dom card -> ( ( B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) ) )
34 33 3impib 
 |-  ( ( U. A e. dom card /\ B e. A /\ A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) -> E. x e. A ( B C_ x /\ A. y e. A -. x C. y ) )