Theorem fvmptiunrelexplb1d

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

	Ref	Expression
Hypotheses	fvmptiunrelexplb1d.c	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
	fvmptiunrelexplb1d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
	fvmptiunrelexplb1d.n	⊢ ( 𝜑 → 𝑁 ∈ V )
	fvmptiunrelexplb1d.1	⊢ ( 𝜑 → 1 ∈ 𝑁 )
Assertion	fvmptiunrelexplb1d	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝐶 ‘ 𝑅 ) )

Proof

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