Theorem ovmptss

Description: If all the values of the mapping are subsets of a class X , then so is any evaluation of the mapping. (Contributed by Mario Carneiro, 24-Dec-2016) Avoid ax-un and shorten proof. (Revised by Zhi Wang, 16-Sep-2026)

	Ref	Expression
Hypothesis	ovmptss.1	|- F = ( x e. A , y e. B |-> C )
Assertion	ovmptss	|- ( A. x e. A A. y e. B C C_ X -> ( E F G ) C_ X )

Proof

Step	Hyp	Ref	Expression
1		ovmptss.1	|- F = ( x e. A , y e. B |-> C )
2		ovssunirn	|- ( E ( x e. A , y e. B |-> C ) G ) C_ U. ran ( x e. A , y e. B |-> C )
3		sseq1	|- ( z = C -> ( z C_ X <-> C C_ X ) )
4	3	biimprd	|- ( z = C -> ( C C_ X -> z C_ X ) )
5	4	com12	|- ( C C_ X -> ( z = C -> z C_ X ) )
6	5	2ralimi	|- ( A. x e. A A. y e. B C C_ X -> A. x e. A A. y e. B ( z = C -> z C_ X ) )
7		r19.23v	|- ( A. y e. B ( z = C -> z C_ X ) <-> ( E. y e. B z = C -> z C_ X ) )
8	7	ralbii	|- ( A. x e. A A. y e. B ( z = C -> z C_ X ) <-> A. x e. A ( E. y e. B z = C -> z C_ X ) )
9		r19.23v	|- ( A. x e. A ( E. y e. B z = C -> z C_ X ) <-> ( E. x e. A E. y e. B z = C -> z C_ X ) )
10	8 9	bitri	|- ( A. x e. A A. y e. B ( z = C -> z C_ X ) <-> ( E. x e. A E. y e. B z = C -> z C_ X ) )
11	6 10	sylib	|- ( A. x e. A A. y e. B C C_ X -> ( E. x e. A E. y e. B z = C -> z C_ X ) )
12		eqid	|- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
13	12	rnmpo	|- ran ( x e. A , y e. B |-> C ) = { z | E. x e. A E. y e. B z = C }
14	13	eleq2i	|- ( z e. ran ( x e. A , y e. B |-> C ) <-> z e. { z | E. x e. A E. y e. B z = C } )
15		abid	|- ( z e. { z | E. x e. A E. y e. B z = C } <-> E. x e. A E. y e. B z = C )
16	14 15	bitri	|- ( z e. ran ( x e. A , y e. B |-> C ) <-> E. x e. A E. y e. B z = C )
17	16	imbi1i	|- ( ( z e. ran ( x e. A , y e. B |-> C ) -> z C_ X ) <-> ( E. x e. A E. y e. B z = C -> z C_ X ) )
18	11 17	sylibr	|- ( A. x e. A A. y e. B C C_ X -> ( z e. ran ( x e. A , y e. B |-> C ) -> z C_ X ) )
19	18	ralrimiv	|- ( A. x e. A A. y e. B C C_ X -> A. z e. ran ( x e. A , y e. B |-> C ) z C_ X )
20		unissb	|- ( U. ran ( x e. A , y e. B |-> C ) C_ X <-> A. z e. ran ( x e. A , y e. B |-> C ) z C_ X )
21	19 20	sylibr	|- ( A. x e. A A. y e. B C C_ X -> U. ran ( x e. A , y e. B |-> C ) C_ X )
22	2 21	sstrid	|- ( A. x e. A A. y e. B C C_ X -> ( E ( x e. A , y e. B |-> C ) G ) C_ X )
23	1	oveqi	|- ( E F G ) = ( E ( x e. A , y e. B |-> C ) G )
24	23	sseq1i	|- ( ( E F G ) C_ X <-> ( E ( x e. A , y e. B |-> C ) G ) C_ X )
25	22 24	sylibr	|- ( A. x e. A A. y e. B C C_ X -> ( E F G ) C_ X )