Metamath Proof Explorer

Theorem iunrelexpmin2

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

Ref Expression
Hypothesis iunrelexpmin2.def 
|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
Assertion iunrelexpmin2 
|- ( ( R e. V /\ N = NN0 ) -> A. s ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )

Proof

Step Hyp Ref Expression
1 iunrelexpmin2.def 
 |-  C = ( r e. _V |-> U_ n e. N ( r ^r n ) )
2 simplr 
 |-  ( ( ( R e. V /\ N = NN0 ) /\ r = R ) -> N = NN0 )
3 simpr 
 |-  ( ( ( R e. V /\ N = NN0 ) /\ r = R ) -> r = R )
4 3 oveq1d 
 |-  ( ( ( R e. V /\ N = NN0 ) /\ r = R ) -> ( r ^r n ) = ( R ^r n ) )
5 2 4 iuneq12d 
 |-  ( ( ( R e. V /\ N = NN0 ) /\ r = R ) -> U_ n e. N ( r ^r n ) = U_ n e. NN0 ( R ^r n ) )
6 elex 
 |-  ( R e. V -> R e. _V )
7 6 adantr 
 |-  ( ( R e. V /\ N = NN0 ) -> R e. _V )
8 nn0ex 
 |-  NN0 e. _V
9 ovex 
 |-  ( R ^r n ) e. _V
10 8 9 iunex 
 |-  U_ n e. NN0 ( R ^r n ) e. _V
11 10 a1i 
 |-  ( ( R e. V /\ N = NN0 ) -> U_ n e. NN0 ( R ^r n ) e. _V )
12 1 5 7 11 fvmptd2 
 |-  ( ( R e. V /\ N = NN0 ) -> ( C ` R ) = U_ n e. NN0 ( R ^r n ) )
13 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
14 13 sseq1d 
 |-  ( R e. V -> ( ( R ^r 0 ) C_ s <-> ( _I |` ( dom R u. ran R ) ) C_ s ) )
15 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
16 15 sseq1d 
 |-  ( R e. V -> ( ( R ^r 1 ) C_ s <-> R C_ s ) )
17 14 16 3anbi12d 
 |-  ( R e. V -> ( ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) <-> ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) ) )
18 elnn0 
 |-  ( n e. NN0 <-> ( n e. NN \/ n = 0 ) )
19 oveq2 
 |-  ( x = 1 -> ( R ^r x ) = ( R ^r 1 ) )
20 19 sseq1d 
 |-  ( x = 1 -> ( ( R ^r x ) C_ s <-> ( R ^r 1 ) C_ s ) )
21 20 imbi2d 
 |-  ( x = 1 -> ( ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r 1 ) C_ s ) ) )
22 oveq2 
 |-  ( x = y -> ( R ^r x ) = ( R ^r y ) )
23 22 sseq1d 
 |-  ( x = y -> ( ( R ^r x ) C_ s <-> ( R ^r y ) C_ s ) )
24 23 imbi2d 
 |-  ( x = y -> ( ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r y ) C_ s ) ) )
25 oveq2 
 |-  ( x = ( y + 1 ) -> ( R ^r x ) = ( R ^r ( y + 1 ) ) )
26 25 sseq1d 
 |-  ( x = ( y + 1 ) -> ( ( R ^r x ) C_ s <-> ( R ^r ( y + 1 ) ) C_ s ) )
27 26 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r ( y + 1 ) ) C_ s ) ) )
28 oveq2 
 |-  ( x = n -> ( R ^r x ) = ( R ^r n ) )
29 28 sseq1d 
 |-  ( x = n -> ( ( R ^r x ) C_ s <-> ( R ^r n ) C_ s ) )
30 29 imbi2d 
 |-  ( x = n -> ( ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r x ) C_ s ) <-> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r n ) C_ s ) ) )
31 simpr2 
 |-  ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r 1 ) C_ s )
32 simp1 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> y e. NN )
33 1nn 
 |-  1 e. NN
34 33 a1i 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> 1 e. NN )
35 simp2l 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> R e. V )
36 relexpaddnn 
 |-  ( ( y e. NN /\ 1 e. NN /\ R e. V ) -> ( ( R ^r y ) o. ( R ^r 1 ) ) = ( R ^r ( y + 1 ) ) )
37 32 34 35 36 syl3anc 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( 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 ) ) )
38 simp2r3 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( s o. s ) C_ s )
39 simp3 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( R ^r y ) C_ s )
40 simp2r2 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( R ^r 1 ) C_ s )
41 38 39 40 trrelssd 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( ( R ^r y ) o. ( R ^r 1 ) ) C_ s )
42 37 41 eqsstrrd 
 |-  ( ( y e. NN /\ ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) /\ ( R ^r y ) C_ s ) -> ( R ^r ( y + 1 ) ) C_ s )
43 42 3exp 
 |-  ( y e. NN -> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( ( R ^r y ) C_ s -> ( R ^r ( y + 1 ) ) C_ s ) ) )
44 43 a2d 
 |-  ( y e. NN -> ( ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r y ) C_ s ) -> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r ( y + 1 ) ) C_ s ) ) )
45 21 24 27 30 31 44 nnind 
 |-  ( n e. NN -> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r n ) C_ s ) )
46 simpr1 
 |-  ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r 0 ) C_ s )
47 oveq2 
 |-  ( n = 0 -> ( R ^r n ) = ( R ^r 0 ) )
48 47 sseq1d 
 |-  ( n = 0 -> ( ( R ^r n ) C_ s <-> ( R ^r 0 ) C_ s ) )
49 46 48 syl5ibr 
 |-  ( n = 0 -> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r n ) C_ s ) )
50 45 49 jaoi 
 |-  ( ( n e. NN \/ n = 0 ) -> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r n ) C_ s ) )
51 18 50 sylbi 
 |-  ( n e. NN0 -> ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( R ^r n ) C_ s ) )
52 51 com12 
 |-  ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> ( n e. NN0 -> ( R ^r n ) C_ s ) )
53 52 ralrimiv 
 |-  ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> A. n e. NN0 ( R ^r n ) C_ s )
54 iunss 
 |-  ( U_ n e. NN0 ( R ^r n ) C_ s <-> A. n e. NN0 ( R ^r n ) C_ s )
55 53 54 sylibr 
 |-  ( ( R e. V /\ ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) ) -> U_ n e. NN0 ( R ^r n ) C_ s )
56 55 ex 
 |-  ( R e. V -> ( ( ( R ^r 0 ) C_ s /\ ( R ^r 1 ) C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN0 ( R ^r n ) C_ s ) )
57 17 56 sylbird 
 |-  ( R e. V -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN0 ( R ^r n ) C_ s ) )
58 57 adantr 
 |-  ( ( R e. V /\ N = NN0 ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN0 ( R ^r n ) C_ s ) )
59 sseq1 
 |-  ( ( C ` R ) = U_ n e. NN0 ( R ^r n ) -> ( ( C ` R ) C_ s <-> U_ n e. NN0 ( R ^r n ) C_ s ) )
60 59 imbi2d 
 |-  ( ( C ` R ) = U_ n e. NN0 ( R ^r n ) -> ( ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) <-> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN0 ( R ^r n ) C_ s ) ) )
61 58 60 syl5ibr 
 |-  ( ( C ` R ) = U_ n e. NN0 ( R ^r n ) -> ( ( R e. V /\ N = NN0 ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) ) )
62 12 61 mpcom 
 |-  ( ( R e. V /\ N = NN0 ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )
63 62 alrimiv 
 |-  ( ( R e. V /\ N = NN0 ) -> A. s ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )