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		brcogw	⊢ ( ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ∧ 𝑦 ∈ V ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) → 𝑥 ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) 𝑧 )
19	18	ex	⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ∧ 𝑦 ∈ V ) → ( ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → 𝑥 ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) 𝑧 ) )
20	15 16 17 19	mp3an	⊢ ( ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → 𝑥 ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) 𝑧 )
21		simpll3	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
22		simprr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
23		simpll2	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑁 = ( ℤ≥ ‘ 𝑀 ) )
24	22 23	eleqtrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
25		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ℕ0 )
26	21 24 25	syl2anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ ℕ0 )
27		simprl	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
28	27 23	eleqtrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
29	21 28 9	syl2anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ ℕ0 )
30		simpll1	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ 𝑉 )
31		relexpaddss	⊢ ( ( 𝑗 ∈ ℕ0 ∧ 𝑖 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑗 + 𝑖 ) ) )
32	26 29 30 31	syl3anc	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑗 + 𝑖 ) ) )
33		simplr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑛 = ( 𝑗 + 𝑖 ) )
34	33	oveq2d	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑗 + 𝑖 ) ) )
35	32 34	sseqtrrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) ⊆ ( 𝑅 ↑𝑟 𝑛 ) )
36	35	ssbrd	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑥 ( ( 𝑅 ↑𝑟 𝑗 ) ∘ ( 𝑅 ↑𝑟 𝑖 ) ) 𝑧 → 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
37	20 36	syl5	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
38	37	impr	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 )
39	14 38	jca	⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) ∧ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) ) → ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
40	39	ex	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 = ( 𝑗 + 𝑖 ) ) → ( ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) → ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
41	2 40	spcimedv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) → ∃ 𝑛 ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
42	41	exlimdvv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) → ∃ 𝑛 ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
43		reeanv	⊢ ( ∃ 𝑖 ∈ 𝑁 ∃ 𝑗 ∈ 𝑁 ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ↔ ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) )
44		r2ex	⊢ ( ∃ 𝑖 ∈ 𝑁 ∃ 𝑗 ∈ 𝑁 ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ↔ ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) )
45	43 44	bitr3i	⊢ ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ↔ ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) )
46		df-rex	⊢ ( ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ↔ ∃ 𝑛 ( 𝑛 ∈ 𝑁 ∧ 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
47	42 45 46	3imtr4g	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
48	47	alrimiv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
49	48	alrimiv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
50	49	alrimiv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
51		cotr	⊢ ( ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) )
52	1	briunov2uz	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ↔ ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑦 ) )
53		oveq2	⊢ ( 𝑛 = 𝑖 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑖 ) )
54	53	breqd	⊢ ( 𝑛 = 𝑖 → ( 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑦 ↔ 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ) )
55	54	cbvrexvw	⊢ ( ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑦 ↔ ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 )
56	52 55	bitrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ↔ ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ) )
57	1	briunov2uz	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ↔ ∃ 𝑛 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
58		oveq2	⊢ ( 𝑛 = 𝑗 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑗 ) )
59	58	breqd	⊢ ( 𝑛 = 𝑗 → ( 𝑦 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ↔ 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) )
60	59	cbvrexvw	⊢ ( ∃ 𝑛 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ↔ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 )
61	57 60	bitrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ↔ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) )
62	56 61	anbi12d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) ) )
63	1	briunov2uz	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ↔ ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) )
64	62 63	imbi12d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
65	64	albidv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑧 ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
66	65	albidv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
67	66	albidv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑦 ∧ 𝑦 ( 𝐶 ‘ 𝑅 ) 𝑧 ) → 𝑥 ( 𝐶 ‘ 𝑅 ) 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
68	51 67	syl5bb	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) ) )
69	68	biimprd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) → ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ) )
70	69	3adant3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑖 ) 𝑦 ∧ ∃ 𝑗 ∈ 𝑁 𝑦 ( 𝑅 ↑𝑟 𝑗 ) 𝑧 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ( 𝑅 ↑𝑟 𝑛 ) 𝑧 ) → ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) ) )
71	50 70	mpd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐶 ‘ 𝑅 ) ∘ ( 𝐶 ‘ 𝑅 ) ) ⊆ ( 𝐶 ‘ 𝑅 ) )