Metamath Proof Explorer


Theorem briunov2

Description: Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the two classes are related by that operator value. (Contributed by RP, 1-Jun-2020)

Ref Expression
Hypothesis briunov2.def
|- C = ( r e. _V |-> U_ n e. N ( r .^ n ) )
Assertion briunov2
|- ( ( R e. U /\ N e. V ) -> ( X ( C ` R ) Y <-> E. n e. N X ( R .^ n ) Y ) )

Proof

Step Hyp Ref Expression
1 briunov2.def
 |-  C = ( r e. _V |-> U_ n e. N ( r .^ n ) )
2 1 eliunov2
 |-  ( ( R e. U /\ N e. V ) -> ( <. X , Y >. e. ( C ` R ) <-> E. n e. N <. X , Y >. e. ( R .^ n ) ) )
3 df-br
 |-  ( X ( C ` R ) Y <-> <. X , Y >. e. ( C ` R ) )
4 df-br
 |-  ( X ( R .^ n ) Y <-> <. X , Y >. e. ( R .^ n ) )
5 4 rexbii
 |-  ( E. n e. N X ( R .^ n ) Y <-> E. n e. N <. X , Y >. e. ( R .^ n ) )
6 2 3 5 3bitr4g
 |-  ( ( R e. U /\ N e. V ) -> ( X ( C ` R ) Y <-> E. n e. N X ( R .^ n ) Y ) )