Theorem 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	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
Assertion	iunrelexpuztr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		mptiunrelexp.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
2		ovexd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑗 + 𝑖 ) ∈ V )
3		simprlr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑗 ∈ 𝑁 )
4		simpll2	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑁 = ( ℤ≥ ‘ 𝑀 ) )
5	3 4	eleqtrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
6		simpll3	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑀 ∈ ℕ0 )
7		simprll	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑖 ∈ 𝑁 )
8	7 4	eleqtrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
9		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ℕ0 )
10	6 8 9	syl2anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑖 ∈ ℕ0 )
11		uzaddcl	⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑗 + 𝑖 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
12	5 10 11	syl2anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → ( 𝑗 + 𝑖 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
13		simplr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑛 = ( 𝑗 + 𝑖 ) )
14	12 13 4	3eltr4d	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑛 ∈ 𝑁 )
15		vex	⊢ 𝑥 ∈ V
16		vex	⊢ 𝑦 ∈ V
17		vex	⊢ 𝑧 ∈ V
18	15 16 17	brcoi	⊢ ( ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → 𝑥 ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) 𝑧 )
19		simpll3	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
20		simprr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
21		simpll2	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑁 = ( ℤ≥ ‘ 𝑀 ) )
22	20 21	eleqtrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
23		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ℕ0 )
24	19 22 23	syl2anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ ℕ0 )
25		simprl	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
26	25 21	eleqtrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
27	19 26 9	syl2anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ ℕ0 )
28		simpll1	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ 𝑉 )
29		relexpaddss	⊢ ( ( 𝑗 ∈ ℕ0 ∧ 𝑖 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑗 + 𝑖 ) ) )
30	24 27 28 29	syl3anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑗 + 𝑖 ) ) )
31		simplr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑛 = ( 𝑗 + 𝑖 ) )
32	31	oveq2d	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑗 + 𝑖 ) ) )
33	30 32	sseqtrrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) ⊆ ( 𝑅 ↑𝑟 𝑛 ) )
34	33	ssbrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑥 ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) 𝑧 → 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
35	18 34	syl5	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
36	35	impr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 )
37	14 36	jca	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
38	37	ex	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) → ( ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) → ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
39	2 38	spcimedv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) → ∃ 𝑛 ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
40	39	exlimdvv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) → ∃ 𝑛 ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
41		reeanv	⊢ ( ∃ 𝑖 ∈ 𝑁 ∃ 𝑗 ∈ 𝑁 ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ↔ ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) )
42		r2ex	⊢ ( ∃ 𝑖 ∈ 𝑁 ∃ 𝑗 ∈ 𝑁 ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ↔ ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) )
43	41 42	bitr3i	⊢ ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ↔ ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) )
44		df-rex	⊢ ( ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ↔ ∃ 𝑛 ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
45	40 43 44	3imtr4g	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
46	45	alrimiv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
47	46	alrimiv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
48	47	alrimiv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
49		cotr	⊢ ( ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) )
50	1	briunov2uz	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ↔ ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑦 ) )
51		oveq2	⊢ ( 𝑛 = 𝑖 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑖 ) )
52	51	breqd	⊢ ( 𝑛 = 𝑖 → ( 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑦 ↔ 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ) )
53	52	cbvrexvw	⊢ ( ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑦 ↔ ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 )
54	50 53	bitrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ↔ ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ) )
55	1	briunov2uz	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ↔ ∃ 𝑛 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
56		oveq2	⊢ ( 𝑛 = 𝑗 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑗 ) )
57	56	breqd	⊢ ( 𝑛 = 𝑗 → ( 𝑦 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ↔ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) )
58	57	cbvrexvw	⊢ ( ∃ 𝑛 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ↔ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 )
59	55 58	bitrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ↔ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) )
60	54 59	anbi12d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) )
61	1	briunov2uz	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ↔ ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
62	60 61	imbi12d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
63	62	albidv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑧 ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
64	63	2albidv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
65	49 64	bitrid	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
66	65	biimprd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) → ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ) )
67	66	3adant3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) → ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ) )
68	48 67	mpd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) )