Metamath Proof Explorer

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	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
		fvmptiunrelexplb1d.r	$⊢ φ \to R \in V$
		fvmptiunrelexplb1d.n	$⊢ φ \to N \in V$
		fvmptiunrelexplb1d.1	$⊢ φ \to 1 \in N$
	Assertion	fvmptiunrelexplb1d	$⊢ φ \to R \subseteq C (R)$

Proof

Step	Hyp	Ref	Expression
1		fvmptiunrelexplb1d.c	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
2		fvmptiunrelexplb1d.r	$⊢ φ \to R \in V$
3		fvmptiunrelexplb1d.n	$⊢ φ \to N \in V$
4		fvmptiunrelexplb1d.1	$⊢ φ \to 1 \in N$
5		oveq2	$⊢ n = 1 \to R ↑_{r} n = R ↑_{r} 1$
6	5	ssiun2s	$⊢ 1 \in N \to R ↑_{r} 1 \subseteq ⋃_{n \in N} (R ↑_{r} n)$
7	4 6	syl	$⊢ φ \to R ↑_{r} 1 \subseteq ⋃_{n \in N} (R ↑_{r} n)$
8	2	relexp1d	$⊢ φ \to R ↑_{r} 1 = R$
9		oveq1	$⊢ r = R \to r ↑_{r} n = R ↑_{r} n$
10	9	iuneq2d	$⊢ r = R \to ⋃_{n \in N} (r ↑_{r} n) = ⋃_{n \in N} (R ↑_{r} n)$
11		ovex	$⊢ R ↑_{r} n \in V$
12	11	rgenw	$⊢ \forall n \in N R ↑_{r} n \in V$
13		iunexg	$⊢ (N \in V \land \forall n \in N R ↑_{r} n \in V) \to ⋃_{n \in N} (R ↑_{r} n) \in V$
14	3 12 13	sylancl	$⊢ φ \to ⋃_{n \in N} (R ↑_{r} n) \in V$
15	1 10 2 14	fvmptd3	$⊢ φ \to C (R) = ⋃_{n \in N} (R ↑_{r} n)$
16	15	eqcomd	$⊢ φ \to ⋃_{n \in N} (R ↑_{r} n) = C (R)$
17	7 8 16	3sstr3d	$⊢ φ \to R \subseteq C (R)$