iunrelexpuztr

Description: The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 . (Contributed by RP, 4-Jun-2020)

		Ref	Expression
	Hypothesis	mptiunrelexp.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
	Assertion	iunrelexpuztr	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to C (R) \circ C (R) \subseteq C (R)$

Proof

Step	Hyp	Ref	Expression
1		mptiunrelexp.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
2		ovexd	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to j + i \in V$
3		simprlr	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to j \in N$
4		simpll2	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to N = ℤ_{\geq M}$
5	3 4	eleqtrd	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to j \in ℤ_{\geq M}$
6		simpll3	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to M \in ℕ_{0}$
7		simprll	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to i \in N$
8	7 4	eleqtrd	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to i \in ℤ_{\geq M}$
9		eluznn0	$⊢ (M \in ℕ_{0} \land i \in ℤ_{\geq M}) \to i \in ℕ_{0}$
10	6 8 9	syl2anc	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to i \in ℕ_{0}$
11		uzaddcl	$⊢ (j \in ℤ_{\geq M} \land i \in ℕ_{0}) \to j + i \in ℤ_{\geq M}$
12	5 10 11	syl2anc	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to j + i \in ℤ_{\geq M}$
13		simplr	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to n = j + i$
14	12 13 4	3eltr4d	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to n \in N$
15		vex	$⊢ x \in V$
16		vex	$⊢ y \in V$
17		vex	$⊢ z \in V$
18	15 16 17	brcoi	$⊢ (x (R ↑_{r} i) y \land y (R ↑_{r} j) z) \to x ((R ↑_{r} j) \circ (R ↑_{r} i)) z$
19		simpll3	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to M \in ℕ_{0}$
20		simprr	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to j \in N$
21		simpll2	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to N = ℤ_{\geq M}$
22	20 21	eleqtrd	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to j \in ℤ_{\geq M}$
23		eluznn0	$⊢ (M \in ℕ_{0} \land j \in ℤ_{\geq M}) \to j \in ℕ_{0}$
24	19 22 23	syl2anc	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to j \in ℕ_{0}$
25		simprl	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to i \in N$
26	25 21	eleqtrd	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to i \in ℤ_{\geq M}$
27	19 26 9	syl2anc	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to i \in ℕ_{0}$
28		simpll1	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to R \in V$
29		relexpaddss	$⊢ (j \in ℕ_{0} \land i \in ℕ_{0} \land R \in V) \to (R ↑_{r} j) \circ (R ↑_{r} i) \subseteq R ↑_{r} (j + i)$
30	24 27 28 29	syl3anc	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to (R ↑_{r} j) \circ (R ↑_{r} i) \subseteq R ↑_{r} (j + i)$
31		simplr	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to n = j + i$
32	31	oveq2d	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to R ↑_{r} n = R ↑_{r} (j + i)$
33	30 32	sseqtrrd	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to (R ↑_{r} j) \circ (R ↑_{r} i) \subseteq R ↑_{r} n$
34	33	ssbrd	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to (x ((R ↑_{r} j) \circ (R ↑_{r} i)) z \to x (R ↑_{r} n) z)$
35	18 34	syl5	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land (i \in N \land j \in N)) \to ((x (R ↑_{r} i) y \land y (R ↑_{r} j) z) \to x (R ↑_{r} n) z)$
36	35	impr	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to x (R ↑_{r} n) z$
37	14 36	jca	$⊢ (((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \land ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))) \to (n \in N \land x (R ↑_{r} n) z)$
38	37	ex	$⊢ ((R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \land n = j + i) \to (((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z)) \to (n \in N \land x (R ↑_{r} n) z))$
39	2 38	spcimedv	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to (((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z)) \to \exists n (n \in N \land x (R ↑_{r} n) z))$
40	39	exlimdvv	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to (\exists i \exists j ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z)) \to \exists n (n \in N \land x (R ↑_{r} n) z))$
41		reeanv	$⊢ \exists i \in N \exists j \in N (x (R ↑_{r} i) y \land y (R ↑_{r} j) z) \leftrightarrow (\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z)$
42		r2ex	$⊢ \exists i \in N \exists j \in N (x (R ↑_{r} i) y \land y (R ↑_{r} j) z) \leftrightarrow \exists i \exists j ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))$
43	41 42	bitr3i	$⊢ (\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \leftrightarrow \exists i \exists j ((i \in N \land j \in N) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z))$
44		df-rex	$⊢ \exists n \in N x (R ↑_{r} n) z \leftrightarrow \exists n (n \in N \land x (R ↑_{r} n) z)$
45	40 43 44	3imtr4g	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z)$
46	45	alrimiv	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z)$
47	46	alrimiv	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to \forall y \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z)$
48	47	alrimiv	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to \forall x \forall y \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z)$
49		cotr	$⊢ C (R) \circ C (R) \subseteq C (R) \leftrightarrow \forall x \forall y \forall z ((x C (R) y \land y C (R) z) \to x C (R) z)$
50	1	briunov2uz	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (x C (R) y \leftrightarrow \exists n \in N x (R ↑_{r} n) y)$
51		oveq2	$⊢ n = i \to R ↑_{r} n = R ↑_{r} i$
52	51	breqd	$⊢ n = i \to (x (R ↑_{r} n) y \leftrightarrow x (R ↑_{r} i) y)$
53	52	cbvrexvw	$⊢ \exists n \in N x (R ↑_{r} n) y \leftrightarrow \exists i \in N x (R ↑_{r} i) y$
54	50 53	bitrdi	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (x C (R) y \leftrightarrow \exists i \in N x (R ↑_{r} i) y)$
55	1	briunov2uz	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (y C (R) z \leftrightarrow \exists n \in N y (R ↑_{r} n) z)$
56		oveq2	$⊢ n = j \to R ↑_{r} n = R ↑_{r} j$
57	56	breqd	$⊢ n = j \to (y (R ↑_{r} n) z \leftrightarrow y (R ↑_{r} j) z)$
58	57	cbvrexvw	$⊢ \exists n \in N y (R ↑_{r} n) z \leftrightarrow \exists j \in N y (R ↑_{r} j) z$
59	55 58	bitrdi	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (y C (R) z \leftrightarrow \exists j \in N y (R ↑_{r} j) z)$
60	54 59	anbi12d	$⊢ (R \in V \land N = ℤ_{\geq M}) \to ((x C (R) y \land y C (R) z) \leftrightarrow (\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z))$
61	1	briunov2uz	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (x C (R) z \leftrightarrow \exists n \in N x (R ↑_{r} n) z)$
62	60 61	imbi12d	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (((x C (R) y \land y C (R) z) \to x C (R) z) \leftrightarrow ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z))$
63	62	albidv	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (\forall z ((x C (R) y \land y C (R) z) \to x C (R) z) \leftrightarrow \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z))$
64	63	2albidv	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (\forall x \forall y \forall z ((x C (R) y \land y C (R) z) \to x C (R) z) \leftrightarrow \forall x \forall y \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z))$
65	49 64	bitrid	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (C (R) \circ C (R) \subseteq C (R) \leftrightarrow \forall x \forall y \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z))$
66	65	biimprd	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (\forall x \forall y \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z) \to C (R) \circ C (R) \subseteq C (R))$
67	66	3adant3	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to (\forall x \forall y \forall z ((\exists i \in N x (R ↑_{r} i) y \land \exists j \in N y (R ↑_{r} j) z) \to \exists n \in N x (R ↑_{r} n) z) \to C (R) \circ C (R) \subseteq C (R))$
68	48 67	mpd	$⊢ (R \in V \land N = ℤ_{\geq M} \land M \in ℕ_{0}) \to C (R) \circ C (R) \subseteq C (R)$

Metamath Proof Explorer

Theorem iunrelexpuztr

Proof