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)

		Ref	Expression
	Hypothesis	ovmptss.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	Assertion	ovmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ( 𝐸 𝐹 𝐺 ) ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ovmptss.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		mpomptsx	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
3	1 2	eqtri	⊢ 𝐹 = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
4	3	fvmptss	⊢ ( ∀ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ⊆ 𝑋 → ( 𝐹 ‘ ⟨ 𝐸 , 𝐺 ⟩ ) ⊆ 𝑋 )
5		vex	⊢ 𝑢 ∈ V
6		vex	⊢ 𝑣 ∈ V
7	5 6	op1std	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑢 )
8	7	csbeq1d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
9	5 6	op2ndd	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2^nd ‘ 𝑧 ) = 𝑣 )
10	9	csbeq1d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
11	10	csbeq2dv	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ 𝑢 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
12	8 11	eqtrd	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
13	12	sseq1d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ↔ ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ) )
14	13	raliunxp	⊢ ( ∀ 𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 )
15		nfcv	⊢ Ⅎ 𝑢 ( { 𝑥 } × 𝐵 )
16		nfcv	⊢ Ⅎ 𝑥 { 𝑢 }
17		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ 𝐵
18	16 17	nfxp	⊢ Ⅎ 𝑥 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
19		sneq	⊢ ( 𝑥 = 𝑢 → { 𝑥 } = { 𝑢 } )
20		csbeq1a	⊢ ( 𝑥 = 𝑢 → 𝐵 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
21	19 20	xpeq12d	⊢ ( 𝑥 = 𝑢 → ( { 𝑥 } × 𝐵 ) = ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) )
22	15 18 21	cbviun	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
23	22	raleqi	⊢ ( ∀ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ↔ ∀ 𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ⊆ 𝑋 )
24		nfv	⊢ Ⅎ 𝑢 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋
25		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶
26		nfcv	⊢ Ⅎ 𝑥 𝑋
27	25 26	nfss	⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋
28	17 27	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋
29		nfv	⊢ Ⅎ 𝑣 𝐶 ⊆ 𝑋
30		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ 𝐶
31		nfcv	⊢ Ⅎ 𝑦 𝑋
32	30 31	nfss	⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋
33		csbeq1a	⊢ ( 𝑦 = 𝑣 → 𝐶 = ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
34	33	sseq1d	⊢ ( 𝑦 = 𝑣 → ( 𝐶 ⊆ 𝑋 ↔ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ) )
35	29 32 34	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀ 𝑣 ∈ 𝐵 ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 )
36		csbeq1a	⊢ ( 𝑥 = 𝑢 → ⦋ 𝑣 / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
37	36	sseq1d	⊢ ( 𝑥 = 𝑢 → ( ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ↔ ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ) )
38	20 37	raleqbidv	⊢ ( 𝑥 = 𝑢 → ( ∀ 𝑣 ∈ 𝐵 ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ↔ ∀ 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ) )
39	35 38	bitrid	⊢ ( 𝑥 = 𝑢 → ( ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀ 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 ) )
40	24 28 39	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 ⊆ 𝑋 )
41	14 23 40	3bitr4ri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 ↔ ∀ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ⊆ 𝑋 )
42		df-ov	⊢ ( 𝐸 𝐹 𝐺 ) = ( 𝐹 ‘ ⟨ 𝐸 , 𝐺 ⟩ )
43	42	sseq1i	⊢ ( ( 𝐸 𝐹 𝐺 ) ⊆ 𝑋 ↔ ( 𝐹 ‘ ⟨ 𝐸 , 𝐺 ⟩ ) ⊆ 𝑋 )
44	4 41 43	3imtr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → ( 𝐸 𝐹 𝐺 ) ⊆ 𝑋 )

Metamath Proof Explorer

Theorem ovmptss

Proof