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 )