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	$⊢ z \in V$
17		vex	$⊢ y \in V$
18		brcogw	$⊢ ((x \in V \land z \in V \land y \in V) \land (x (R ↑_{r} i) y \land y (R ↑_{r} j) z)) \to x ((R ↑_{r} j) \circ (R ↑_{r} i)) z$
19	18	ex	$⊢ (x \in V \land z \in V \land y \in V) \to ((x (R ↑_{r} i) y \land y (R ↑_{r} j) z) \to x ((R ↑_{r} j) \circ (R ↑_{r} i)) z)$
20	15 16 17 19	mp3an	$⊢ (x (R ↑_{r} i) y \land y (R ↑_{r} j) z) \to x ((R ↑_{r} j) \circ (R ↑_{r} i)) z$
21		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}$
22		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$
23		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}$
24	22 23	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}$
25		eluznn0	$⊢ (M \in ℕ_{0} \land j \in ℤ_{\geq M}) \to j \in ℕ_{0}$
26	21 24 25	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}$
27		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$
28	27 23	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}$
29	21 28 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}$
30		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$
31		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)$
32	26 29 30 31	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)$
33		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$
34	33	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)$
35	32 34	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$
36	35	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)$
37	20 36	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)$
38	37	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$
39	14 38	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)$
40	39	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))$
41	2 40	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))$
42	41	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))$
43		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)$
44		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))$
45	43 44	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))$
46		df-rex	$⊢ \exists n \in N x (R ↑_{r} n) z \leftrightarrow \exists n (n \in N \land x (R ↑_{r} n) z)$
47	42 45 46	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)$
48	47	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)$
49	48	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)$
50	49	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)$
51		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)$
52	1	briunov2uz	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (x C (R) y \leftrightarrow \exists n \in N x (R ↑_{r} n) y)$
53		oveq2	$⊢ n = i \to R ↑_{r} n = R ↑_{r} i$
54	53	breqd	$⊢ n = i \to (x (R ↑_{r} n) y \leftrightarrow x (R ↑_{r} i) y)$
55	54	cbvrexvw	$⊢ \exists n \in N x (R ↑_{r} n) y \leftrightarrow \exists i \in N x (R ↑_{r} i) y$
56	52 55	syl6bb	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (x C (R) y \leftrightarrow \exists i \in N x (R ↑_{r} i) y)$
57	1	briunov2uz	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (y C (R) z \leftrightarrow \exists n \in N y (R ↑_{r} n) z)$
58		oveq2	$⊢ n = j \to R ↑_{r} n = R ↑_{r} j$
59	58	breqd	$⊢ n = j \to (y (R ↑_{r} n) z \leftrightarrow y (R ↑_{r} j) z)$
60	59	cbvrexvw	$⊢ \exists n \in N y (R ↑_{r} n) z \leftrightarrow \exists j \in N y (R ↑_{r} j) z$
61	57 60	syl6bb	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (y C (R) z \leftrightarrow \exists j \in N y (R ↑_{r} j) z)$
62	56 61	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))$
63	1	briunov2uz	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (x C (R) z \leftrightarrow \exists n \in N x (R ↑_{r} n) z)$
64	62 63	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))$
65	64	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))$
66	65	albidv	$⊢ (R \in V \land N = ℤ_{\geq M}) \to (\forall y \forall z ((x C (R) y \land y C (R) z) \to x C (R) z) \leftrightarrow \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))$
67	66	albidv	$⊢ (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))$
68	51 67	syl5bb	$⊢ (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))$
69	68	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))$
70	69	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))$
71	50 70	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