Theorem brmptiunrelexpd

Description: If two elements are connected by an indexed union of relational powers, then they are connected via n instances the relation, for some n . Generalization of dfrtrclrec2 . (Contributed by RP, 21-Jul-2020)

	Ref	Expression
Hypotheses	brmptiunrelexpd.c	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
	brmptiunrelexpd.r	⊢ ( 𝜑 → 𝑅 ∈ V )
	brmptiunrelexpd.n	⊢ ( 𝜑 → 𝑁 ⊆ ℕ0 )
Assertion	brmptiunrelexpd	⊢ ( 𝜑 → ( 𝐴 ( 𝐶 ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ 𝑁 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brmptiunrelexpd.c	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
2		brmptiunrelexpd.r	⊢ ( 𝜑 → 𝑅 ∈ V )
3		brmptiunrelexpd.n	⊢ ( 𝜑 → 𝑁 ⊆ ℕ0 )
4		nn0ex	⊢ ℕ0 ∈ V
5	4	ssex	⊢ ( 𝑁 ⊆ ℕ0 → 𝑁 ∈ V )
6	3 5	syl	⊢ ( 𝜑 → 𝑁 ∈ V )
7	1	briunov2	⊢ ( ( 𝑅 ∈ V ∧ 𝑁 ∈ V ) → ( 𝐴 ( 𝐶 ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ 𝑁 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )
8	2 6 7	syl2anc	⊢ ( 𝜑 → ( 𝐴 ( 𝐶 ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ 𝑁 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )