Theorem fvmptiunrelexplb0da

Description: If the indexed union ranges over the zeroth power of the relation, then a restriction of the identity relation is a subset of the appliction of the function to the relation. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypotheses	fvmptiunrelexplb0da.c	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
	fvmptiunrelexplb0da.r	⊢ ( 𝜑 → 𝑅 ∈ V )
	fvmptiunrelexplb0da.n	⊢ ( 𝜑 → 𝑁 ∈ V )
	fvmptiunrelexplb0da.rel	⊢ ( 𝜑 → Rel 𝑅 )
	fvmptiunrelexplb0da.0	⊢ ( 𝜑 → 0 ∈ 𝑁 )
Assertion	fvmptiunrelexplb0da	⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝐶 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fvmptiunrelexplb0da.c	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
2		fvmptiunrelexplb0da.r	⊢ ( 𝜑 → 𝑅 ∈ V )
3		fvmptiunrelexplb0da.n	⊢ ( 𝜑 → 𝑁 ∈ V )
4		fvmptiunrelexplb0da.rel	⊢ ( 𝜑 → Rel 𝑅 )
5		fvmptiunrelexplb0da.0	⊢ ( 𝜑 → 0 ∈ 𝑁 )
6		relfld	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
7	4 6	syl	⊢ ( 𝜑 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
8	7	reseq2d	⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
9	1 2 3 5	fvmptiunrelexplb0d	⊢ ( 𝜑 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) )
10	8 9	eqsstrd	⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝐶 ‘ 𝑅 ) )