Metamath Proof Explorer

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	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
		fvmptiunrelexplb0d.r	$⊢ φ \to R \in V$
		fvmptiunrelexplb0d.n	$⊢ φ \to N \in V$
		fvmptiunrelexplb0d.0	$⊢ φ \to 0 \in N$
	Assertion	fvmptiunrelexplb0d	$⊢ φ \to {I ↾}_{(dom R \cup ran R)} \subseteq C (R)$

Proof

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