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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion ovmptss ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ( 𝐸 𝐹 𝐺 ) ⊆ 𝑋 )

Proof

Step Hyp Ref Expression
1 ovmptss.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 ovssunirn ⊢ ( 𝐸 ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐺 ) ⊆ ∪ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
3 sseq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 ⊆ 𝑋 ↔ 𝐶 ⊆ 𝑋 ) )
4 3 biimprd ⊢ ( 𝑧 = 𝐶 → ( 𝐶 ⊆ 𝑋 → 𝑧 ⊆ 𝑋 ) )
5 4 com12 ⊢ ( 𝐶 ⊆ 𝑋 → ( 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
6 5 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
7 r19.23v ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
8 7 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
9 r19.23v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
10 8 9 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
11 6 10 sylib ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
12 eqid ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
13 12 rnmpo ⊢ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 }
14 13 eleq2i ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ↔ 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } )
15 abid ⊢ ( 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 )
16 14 15 bitri ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 )
17 16 imbi1i ⊢ ( ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) → 𝑧 ⊆ 𝑋 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ⊆ 𝑋 ) )
18 11 17 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) → 𝑧 ⊆ 𝑋 ) )
19 18 ralrimiv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑧 ⊆ 𝑋 )
20 unissb ⊢ ( ∪ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⊆ 𝑋 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑧 ⊆ 𝑋 )
21 19 20 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ∪ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⊆ 𝑋 )
22 2 21 sstrid ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ( 𝐸 ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐺 ) ⊆ 𝑋 )
23 1 oveqi ⊢ ( 𝐸 𝐹 𝐺 ) = ( 𝐸 ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐺 )
24 23 sseq1i ⊢ ( ( 𝐸 𝐹 𝐺 ) ⊆ 𝑋 ↔ ( 𝐸 ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐺 ) ⊆ 𝑋 )
25 22 24 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ( 𝐸 𝐹 𝐺 ) ⊆ 𝑋 )