Theorem fvmptiunrelexplb0d

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	fvmptiunrelexplb0d.c	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
	fvmptiunrelexplb0d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
	fvmptiunrelexplb0d.n	⊢ ( 𝜑 → 𝑁 ∈ V )
	fvmptiunrelexplb0d.0	⊢ ( 𝜑 → 0 ∈ 𝑁 )
Assertion	fvmptiunrelexplb0d	⊢ ( 𝜑 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fvmptiunrelexplb0d.c	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
2		fvmptiunrelexplb0d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
3		fvmptiunrelexplb0d.n	⊢ ( 𝜑 → 𝑁 ∈ V )
4		fvmptiunrelexplb0d.0	⊢ ( 𝜑 → 0 ∈ 𝑁 )
5		oveq2	⊢ ( 𝑛 = 0 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 0 ) )
6	5	ssiun2s	⊢ ( 0 ∈ 𝑁 → ( 𝑅 ↑𝑟 0 ) ⊆ ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) )
7	4 6	syl	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 0 ) ⊆ ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) )
8		relexp0g	⊢ ( 𝑅 ∈ V → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
9	2 8	syl	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
10		oveq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
11	10	iuneq2d	⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) )
12		ovex	⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
13	12	rgenw	⊢ ∀ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) ∈ V
14		iunexg	⊢ ( ( 𝑁 ∈ V ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) ∈ V ) → ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) ∈ V )
15	3 13 14	sylancl	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) ∈ V )
16	1 11 2 15	fvmptd3	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) )
17	16	eqcomd	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑𝑟 𝑛 ) = ( 𝐶 ‘ 𝑅 ) )
18	7 9 17	3sstr3d	⊢ ( 𝜑 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) )