Theorem wununi

Description: A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	|- ( ph -> U e. WUni )
	wununi.2	|- ( ph -> A e. U )
Assertion	wununi	|- ( ph -> U. A e. U )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	|- ( ph -> U e. WUni )
2		wununi.2	|- ( ph -> A e. U )
3		unieq	|- ( x = A -> U. x = U. A )
4	3	eleq1d	|- ( x = A -> ( U. x e. U <-> U. A e. U ) )
5		iswun	|- ( U e. WUni -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
6	5	ibi	|- ( U e. WUni -> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
7	6	simp3d	|- ( U e. WUni -> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) )
8		simp1	|- ( ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> U. x e. U )
9	8	ralimi	|- ( A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> A. x e. U U. x e. U )
10	1 7 9	3syl	|- ( ph -> A. x e. U U. x e. U )
11	4 10 2	rspcdva	|- ( ph -> U. A e. U )