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	|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
	brmptiunrelexpd.r	|- ( ph -> R e. _V )
	brmptiunrelexpd.n	|- ( ph -> N C_ NN0 )
Assertion	brmptiunrelexpd	|- ( ph -> ( A ( C ` R ) B <-> E. n e. N A ( R ^r n ) B ) )

Proof

Step	Hyp	Ref	Expression
1		brmptiunrelexpd.c	|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
2		brmptiunrelexpd.r	|- ( ph -> R e. _V )
3		brmptiunrelexpd.n	|- ( ph -> N C_ NN0 )
4		nn0ex	|- NN0 e. _V
5	4	ssex	|- ( N C_ NN0 -> N e. _V )
6	3 5	syl	|- ( ph -> N e. _V )
7	1	briunov2	|- ( ( R e. _V /\ N e. _V ) -> ( A ( C ` R ) B <-> E. n e. N A ( R ^r n ) B ) )
8	2 6 7	syl2anc	|- ( ph -> ( A ( C ` R ) B <-> E. n e. N A ( R ^r n ) B ) )