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 φ U WUni
wunfi.2 φ A U
wunfi.3 φ A Fin
Assertion wunfi φ A U

Proof

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