Metamath Proof Explorer

Theorem ttukeylem1

Description: Lemma for ttukey . Expand out the property of being an element of a property of finite character. (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 ) )
Assertion ttukeylem1 
|- ( ph -> ( C e. A <-> ( ~P C i^i Fin ) C_ A ) )

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 elex 
 |-  ( C e. A -> C e. _V )
5 4 a1i 
 |-  ( ph -> ( C e. A -> C e. _V ) )
6 id 
 |-  ( ( ~P C i^i Fin ) C_ A -> ( ~P C i^i Fin ) C_ A )
7 ssun1 
 |-  U. A C_ ( U. A u. B )
8 undif1 
 |-  ( ( U. A \ B ) u. B ) = ( U. A u. B )
9 7 8 sseqtrri 
 |-  U. A C_ ( ( U. A \ B ) u. B )
10 fvex 
 |-  ( card ` ( U. A \ B ) ) e. _V
11 f1ofo 
 |-  ( F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) -> F : ( card ` ( U. A \ B ) ) -onto-> ( U. A \ B ) )
12 1 11 syl 
 |-  ( ph -> F : ( card ` ( U. A \ B ) ) -onto-> ( U. A \ B ) )
13 fornex 
 |-  ( ( card ` ( U. A \ B ) ) e. _V -> ( F : ( card ` ( U. A \ B ) ) -onto-> ( U. A \ B ) -> ( U. A \ B ) e. _V ) )
14 10 12 13 mpsyl 
 |-  ( ph -> ( U. A \ B ) e. _V )
15 unexg 
 |-  ( ( ( U. A \ B ) e. _V /\ B e. A ) -> ( ( U. A \ B ) u. B ) e. _V )
16 14 2 15 syl2anc 
 |-  ( ph -> ( ( U. A \ B ) u. B ) e. _V )
17 ssexg 
 |-  ( ( U. A C_ ( ( U. A \ B ) u. B ) /\ ( ( U. A \ B ) u. B ) e. _V ) -> U. A e. _V )
18 9 16 17 sylancr 
 |-  ( ph -> U. A e. _V )
19 uniexb 
 |-  ( A e. _V <-> U. A e. _V )
20 18 19 sylibr 
 |-  ( ph -> A e. _V )
21 ssexg 
 |-  ( ( ( ~P C i^i Fin ) C_ A /\ A e. _V ) -> ( ~P C i^i Fin ) e. _V )
22 6 20 21 syl2anr 
 |-  ( ( ph /\ ( ~P C i^i Fin ) C_ A ) -> ( ~P C i^i Fin ) e. _V )
23 infpwfidom 
 |-  ( ( ~P C i^i Fin ) e. _V -> C ~<_ ( ~P C i^i Fin ) )
24 reldom 
 |-  Rel ~<_
25 24 brrelex1i 
 |-  ( C ~<_ ( ~P C i^i Fin ) -> C e. _V )
26 22 23 25 3syl 
 |-  ( ( ph /\ ( ~P C i^i Fin ) C_ A ) -> C e. _V )
27 26 ex 
 |-  ( ph -> ( ( ~P C i^i Fin ) C_ A -> C e. _V ) )
28 eleq1 
 |-  ( x = C -> ( x e. A <-> C e. A ) )
29 pweq 
 |-  ( x = C -> ~P x = ~P C )
30 29 ineq1d 
 |-  ( x = C -> ( ~P x i^i Fin ) = ( ~P C i^i Fin ) )
31 30 sseq1d 
 |-  ( x = C -> ( ( ~P x i^i Fin ) C_ A <-> ( ~P C i^i Fin ) C_ A ) )
32 28 31 bibi12d 
 |-  ( x = C -> ( ( x e. A <-> ( ~P x i^i Fin ) C_ A ) <-> ( C e. A <-> ( ~P C i^i Fin ) C_ A ) ) )
33 32 spcgv 
 |-  ( C e. _V -> ( A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) -> ( C e. A <-> ( ~P C i^i Fin ) C_ A ) ) )
34 3 33 syl5com 
 |-  ( ph -> ( C e. _V -> ( C e. A <-> ( ~P C i^i Fin ) C_ A ) ) )
35 5 27 34 pm5.21ndd 
 |-  ( ph -> ( C e. A <-> ( ~P C i^i Fin ) C_ A ) )