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 V n N r r n
Assertion iunrelexpmin2 R V N = 0 s I dom R ran R s R s s s s C R s

Proof

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