Description: A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wununi.1 | |- ( ph -> U e. WUni ) |
|
wununi.2 | |- ( ph -> A e. U ) |
||
Assertion | wunint | |- ( ( ph /\ A =/= (/) ) -> |^| A e. U ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wununi.1 | |- ( ph -> U e. WUni ) |
|
2 | wununi.2 | |- ( ph -> A e. U ) |
|
3 | 1 | adantr | |- ( ( ph /\ A =/= (/) ) -> U e. WUni ) |
4 | 1 2 | wununi | |- ( ph -> U. A e. U ) |
5 | 4 | adantr | |- ( ( ph /\ A =/= (/) ) -> U. A e. U ) |
6 | intssuni | |- ( A =/= (/) -> |^| A C_ U. A ) |
|
7 | 6 | adantl | |- ( ( ph /\ A =/= (/) ) -> |^| A C_ U. A ) |
8 | 3 5 7 | wunss | |- ( ( ph /\ A =/= (/) ) -> |^| A e. U ) |