Metamath Proof Explorer

Theorem wunfi

Description: A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses wun0.1 
|- ( ph -> U e. WUni )
wunfi.2 
|- ( ph -> A C_ U )
wunfi.3 
|- ( ph -> A e. Fin )
Assertion wunfi 
|- ( ph -> A e. U )

Proof

Step Hyp Ref Expression
1 wun0.1 
 |-  ( ph -> U e. WUni )
2 wunfi.2 
 |-  ( ph -> A C_ U )
3 wunfi.3 
 |-  ( ph -> A e. Fin )
4 sseq1 
 |-  ( x = (/) -> ( x C_ U <-> (/) C_ U ) )
5 eleq1 
 |-  ( x = (/) -> ( x e. U <-> (/) e. U ) )
6 4 5 imbi12d 
 |-  ( x = (/) -> ( ( x C_ U -> x e. U ) <-> ( (/) C_ U -> (/) e. U ) ) )
7 6 imbi2d 
 |-  ( x = (/) -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( (/) C_ U -> (/) e. U ) ) ) )
8 sseq1 
 |-  ( x = y -> ( x C_ U <-> y C_ U ) )
9 eleq1 
 |-  ( x = y -> ( x e. U <-> y e. U ) )
10 8 9 imbi12d 
 |-  ( x = y -> ( ( x C_ U -> x e. U ) <-> ( y C_ U -> y e. U ) ) )
11 10 imbi2d 
 |-  ( x = y -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( y C_ U -> y e. U ) ) ) )
12 sseq1 
 |-  ( x = ( y u. { z } ) -> ( x C_ U <-> ( y u. { z } ) C_ U ) )
13 eleq1 
 |-  ( x = ( y u. { z } ) -> ( x e. U <-> ( y u. { z } ) e. U ) )
14 12 13 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( x C_ U -> x e. U ) <-> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) )
15 14 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) )
16 sseq1 
 |-  ( x = A -> ( x C_ U <-> A C_ U ) )
17 eleq1 
 |-  ( x = A -> ( x e. U <-> A e. U ) )
18 16 17 imbi12d 
 |-  ( x = A -> ( ( x C_ U -> x e. U ) <-> ( A C_ U -> A e. U ) ) )
19 18 imbi2d 
 |-  ( x = A -> ( ( ph -> ( x C_ U -> x e. U ) ) <-> ( ph -> ( A C_ U -> A e. U ) ) ) )
20 1 wun0 
 |-  ( ph -> (/) e. U )
21 20 a1d 
 |-  ( ph -> ( (/) C_ U -> (/) e. U ) )
22 ssun1 
 |-  y C_ ( y u. { z } )
23 sstr 
 |-  ( ( y C_ ( y u. { z } ) /\ ( y u. { z } ) C_ U ) -> y C_ U )
24 22 23 mpan 
 |-  ( ( y u. { z } ) C_ U -> y C_ U )
25 24 imim1i 
 |-  ( ( y C_ U -> y e. U ) -> ( ( y u. { z } ) C_ U -> y e. U ) )
26 1 adantr 
 |-  ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> U e. WUni )
27 simprr 
 |-  ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> y e. U )
28 simprl 
 |-  ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> ( y u. { z } ) C_ U )
29 28 unssbd 
 |-  ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> { z } C_ U )
30 vex 
 |-  z e. _V
31 30 snss 
 |-  ( z e. U <-> { z } C_ U )
32 29 31 sylibr 
 |-  ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> z e. U )
33 26 32 wunsn 
 |-  ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> { z } e. U )
34 26 27 33 wunun 
 |-  ( ( ph /\ ( ( y u. { z } ) C_ U /\ y e. U ) ) -> ( y u. { z } ) e. U )
35 34 exp32 
 |-  ( ph -> ( ( y u. { z } ) C_ U -> ( y e. U -> ( y u. { z } ) e. U ) ) )
36 35 a2d 
 |-  ( ph -> ( ( ( y u. { z } ) C_ U -> y e. U ) -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) )
37 25 36 syl5 
 |-  ( ph -> ( ( y C_ U -> y e. U ) -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) )
38 37 a2i 
 |-  ( ( ph -> ( y C_ U -> y e. U ) ) -> ( ph -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) )
39 38 a1i 
 |-  ( y e. Fin -> ( ( ph -> ( y C_ U -> y e. U ) ) -> ( ph -> ( ( y u. { z } ) C_ U -> ( y u. { z } ) e. U ) ) ) )
40 7 11 15 19 21 39 findcard2 
 |-  ( A e. Fin -> ( ph -> ( A C_ U -> A e. U ) ) )
41 3 40 mpcom 
 |-  ( ph -> ( A C_ U -> A e. U ) )
42 2 41 mpd 
 |-  ( ph -> A e. U )