Metamath Proof Explorer

Theorem iunrelexpmin1

Description: The indexed union of relation exponentiation over the natural numbers is the minimum transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020)

Ref Expression
Hypothesis iunrelexpmin1.def 
|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
Assertion iunrelexpmin1 
|- ( ( R e. V /\ N = NN ) -> A. s ( ( R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )

Proof

Step Hyp Ref Expression
1 iunrelexpmin1.def 
 |-  C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
2 simplr 
 |-  ( ( ( R e. V /\ N = NN ) /\ r = R ) -> N = NN )
3 simpr 
 |-  ( ( ( R e. V /\ N = NN ) /\ r = R ) -> r = R )
4 3 oveq1d 
 |-  ( ( ( R e. V /\ N = NN ) /\ r = R ) -> ( r ^r n ) = ( R ^r n ) )
5 2 4 iuneq12d 
 |-  ( ( ( R e. V /\ N = NN ) /\ r = R ) -> U_ n e. N ( r ^r n ) = U_ n e. NN ( R ^r n ) )
6 elex 
 |-  ( R e. V -> R e. _V )
7 6 adantr 
 |-  ( ( R e. V /\ N = NN ) -> R e. _V )
8 nnex 
 |-  NN e. _V
9 ovex 
 |-  ( R ^r n ) e. _V
10 8 9 iunex 
 |-  U_ n e. NN ( R ^r n ) e. _V
11 10 a1i 
 |-  ( ( R e. V /\ N = NN ) -> U_ n e. NN ( R ^r n ) e. _V )
12 1 5 7 11 fvmptd2 
 |-  ( ( R e. V /\ N = NN ) -> ( C ` R ) = U_ n e. NN ( R ^r n ) )
13 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
14 13 sseq1d 
 |-  ( R e. V -> ( ( R ^r 1 ) C_ s <-> R C_ s ) )
15 14 anbi1d 
 |-  ( R e. V -> ( ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) <-> ( R C_ s /\ ( s o. s ) C_ s ) ) )
16 oveq2 
 |-  ( x = 1 -> ( R ^r x ) = ( R ^r 1 ) )
17 16 sseq1d 
 |-  ( x = 1 -> ( ( R ^r x ) C_ s <-> ( R ^r 1 ) C_ s ) )
18 17 imbi2d 
 |-  ( x = 1 -> ( ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r 1 ) C_ s ) ) )
19 oveq2 
 |-  ( x = y -> ( R ^r x ) = ( R ^r y ) )
20 19 sseq1d 
 |-  ( x = y -> ( ( R ^r x ) C_ s <-> ( R ^r y ) C_ s ) )
21 20 imbi2d 
 |-  ( x = y -> ( ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r y ) C_ s ) ) )
22 oveq2 
 |-  ( x = ( y + 1 ) -> ( R ^r x ) = ( R ^r ( y + 1 ) ) )
23 22 sseq1d 
 |-  ( x = ( y + 1 ) -> ( ( R ^r x ) C_ s <-> ( R ^r ( y + 1 ) ) C_ s ) )
24 23 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r ( y + 1 ) ) C_ s ) ) )
25 oveq2 
 |-  ( x = n -> ( R ^r x ) = ( R ^r n ) )
26 25 sseq1d 
 |-  ( x = n -> ( ( R ^r x ) C_ s <-> ( R ^r n ) C_ s ) )
27 26 imbi2d 
 |-  ( x = n -> ( ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r n ) C_ s ) ) )
28 simprl 
 |-  ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r 1 ) C_ s )
29 simp1 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> y e. NN )
30 1nn 
 |-  1 e. NN
31 30 a1i 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> 1 e. NN )
32 simp2l 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> R e. V )
33 relexpaddnn 
 |-  ( ( y e. NN /\ 1 e. NN /\ R e. V ) -> ( ( R ^r y ) o. ( R ^r 1 ) ) = ( R ^r ( y + 1 ) ) )
34 29 31 32 33 syl3anc 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( ( R ^r y ) o. ( R ^r 1 ) ) = ( R ^r ( y + 1 ) ) )
35 simp2rr 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( s o. s ) C_ s )
36 simp3 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( R ^r y ) C_ s )
37 simp2rl 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( R ^r 1 ) C_ s )
38 35 36 37 trrelssd 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( ( R ^r y ) o. ( R ^r 1 ) ) C_ s )
39 34 38 eqsstrrd 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( R ^r ( y + 1 ) ) C_ s )
40 39 3exp 
 |-  ( y e. NN -> ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( ( R ^r y ) C_ s -> ( R ^r ( y + 1 ) ) C_ s ) ) )
41 40 a2d 
 |-  ( y e. NN -> ( ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r y ) C_ s ) -> ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r ( y + 1 ) ) C_ s ) ) )
42 18 21 24 27 28 41 nnind 
 |-  ( n e. NN -> ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r n ) C_ s ) )
43 42 com12 
 |-  ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( n e. NN -> ( R ^r n ) C_ s ) )
44 43 ralrimiv 
 |-  ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> A. n e. NN ( R ^r n ) C_ s )
45 iunss 
 |-  ( U_ n e. NN ( R ^r n ) C_ s <-> A. n e. NN ( R ^r n ) C_ s )
46 44 45 sylibr 
 |-  ( ( R e. V /\ ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> U_ n e. NN ( R ^r n ) C_ s )
47 46 ex 
 |-  ( R e. V -> ( ( ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN ( R ^r n ) C_ s ) )
48 15 47 sylbird 
 |-  ( R e. V -> ( ( R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN ( R ^r n ) C_ s ) )
49 48 adantr 
 |-  ( ( R e. V /\ N = NN ) -> ( ( R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN ( R ^r n ) C_ s ) )
50 sseq1 
 |-  ( ( C ` R ) = U_ n e. NN ( R ^r n ) -> ( ( C ` R ) C_ s <-> U_ n e. NN ( R ^r n ) C_ s ) )
51 50 imbi2d 
 |-  ( ( C ` R ) = U_ n e. NN ( R ^r n ) -> ( ( ( R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) <-> ( ( R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN ( R ^r n ) C_ s ) ) )
52 49 51 imbitrrid 
 |-  ( ( C ` R ) = U_ n e. NN ( R ^r n ) -> ( ( R e. V /\ N = NN ) -> ( ( R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) ) )
53 12 52 mpcom 
 |-  ( ( R e. V /\ N = NN ) -> ( ( R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )
54 53 alrimiv 
 |-  ( ( R e. V /\ N = NN ) -> A. s ( ( R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )