Metamath Proof Explorer

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 ∈ A , y ∈ B ⟼ C
Assertion ovmptss ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → E F G ⊆ X

Proof

Step Hyp Ref Expression
1 ovmptss.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 ovssunirn ⊢ E x ∈ A , y ∈ B ⟼ C G ⊆ ⋃ ran ⁡ x ∈ A , y ∈ B ⟼ C
3 sseq1 ⊢ z = C → z ⊆ X ↔ C ⊆ X
4 3 biimprd ⊢ z = C → C ⊆ X → z ⊆ X
5 4 com12 ⊢ C ⊆ X → z = C → z ⊆ X
6 5 2ralimi ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → ∀ x ∈ A ∀ y ∈ B z = C → z ⊆ X
7 r19.23v ⊢ ∀ y ∈ B z = C → z ⊆ X ↔ ∃ y ∈ B z = C → z ⊆ X
8 7 ralbii ⊢ ∀ x ∈ A ∀ y ∈ B z = C → z ⊆ X ↔ ∀ x ∈ A ∃ y ∈ B z = C → z ⊆ X
9 r19.23v ⊢ ∀ x ∈ A ∃ y ∈ B z = C → z ⊆ X ↔ ∃ x ∈ A ∃ y ∈ B z = C → z ⊆ X
10 8 9 bitri ⊢ ∀ x ∈ A ∀ y ∈ B z = C → z ⊆ X ↔ ∃ x ∈ A ∃ y ∈ B z = C → z ⊆ X
11 6 10 sylib ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → ∃ x ∈ A ∃ y ∈ B z = C → z ⊆ X
12 eqid ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ C
13 12 rnmpo ⊢ ran ⁡ x ∈ A , y ∈ B ⟼ C = z | ∃ x ∈ A ∃ y ∈ B z = C
14 13 eleq2i ⊢ z ∈ ran ⁡ x ∈ A , y ∈ B ⟼ C ↔ z ∈ z | ∃ x ∈ A ∃ y ∈ B z = C
15 abid ⊢ z ∈ z | ∃ x ∈ A ∃ y ∈ B z = C ↔ ∃ x ∈ A ∃ y ∈ B z = C
16 14 15 bitri ⊢ z ∈ ran ⁡ x ∈ A , y ∈ B ⟼ C ↔ ∃ x ∈ A ∃ y ∈ B z = C
17 16 imbi1i ⊢ z ∈ ran ⁡ x ∈ A , y ∈ B ⟼ C → z ⊆ X ↔ ∃ x ∈ A ∃ y ∈ B z = C → z ⊆ X
18 11 17 sylibr ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → z ∈ ran ⁡ x ∈ A , y ∈ B ⟼ C → z ⊆ X
19 18 ralrimiv ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → ∀ z ∈ ran ⁡ x ∈ A , y ∈ B ⟼ C z ⊆ X
20 unissb ⊢ ⋃ ran ⁡ x ∈ A , y ∈ B ⟼ C ⊆ X ↔ ∀ z ∈ ran ⁡ x ∈ A , y ∈ B ⟼ C z ⊆ X
21 19 20 sylibr ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → ⋃ ran ⁡ x ∈ A , y ∈ B ⟼ C ⊆ X
22 2 21 sstrid ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → E x ∈ A , y ∈ B ⟼ C G ⊆ X
23 1 oveqi ⊢ E F G = E x ∈ A , y ∈ B ⟼ C G
24 23 sseq1i ⊢ E F G ⊆ X ↔ E x ∈ A , y ∈ B ⟼ C G ⊆ X
25 22 24 sylibr ⊢ ∀ x ∈ A ∀ y ∈ B C ⊆ X → E F G ⊆ X