Metamath Proof Explorer

Theorem relexpindlem

Description: Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Proof shortened by Peter Mazsa, 2-Oct-2022) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypotheses relexpindlem.1 
|- ( et -> Rel R )
relexpindlem.2 
|- ( et -> S e. V )
relexpindlem.3 
|- ( i = S -> ( ph <-> ch ) )
relexpindlem.4 
|- ( i = x -> ( ph <-> ps ) )
relexpindlem.5 
|- ( i = j -> ( ph <-> th ) )
relexpindlem.6 
|- ( et -> ch )
relexpindlem.7 
|- ( et -> ( j R x -> ( th -> ps ) ) )
Assertion relexpindlem 
|- ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) )

Proof

Step Hyp Ref Expression
1 relexpindlem.1 
 |-  ( et -> Rel R )
2 relexpindlem.2 
 |-  ( et -> S e. V )
3 relexpindlem.3 
 |-  ( i = S -> ( ph <-> ch ) )
4 relexpindlem.4 
 |-  ( i = x -> ( ph <-> ps ) )
5 relexpindlem.5 
 |-  ( i = j -> ( ph <-> th ) )
6 relexpindlem.6 
 |-  ( et -> ch )
7 relexpindlem.7 
 |-  ( et -> ( j R x -> ( th -> ps ) ) )
8 eleq1 
 |-  ( k = 0 -> ( k e. NN0 <-> 0 e. NN0 ) )
9 8 anbi2d 
 |-  ( k = 0 -> ( ( ( et /\ R e. _V ) /\ k e. NN0 ) <-> ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) )
10 oveq2 
 |-  ( k = 0 -> ( R ^r k ) = ( R ^r 0 ) )
11 10 breqd 
 |-  ( k = 0 -> ( S ( R ^r k ) x <-> S ( R ^r 0 ) x ) )
12 11 imbi1d 
 |-  ( k = 0 -> ( ( S ( R ^r k ) x -> ps ) <-> ( S ( R ^r 0 ) x -> ps ) ) )
13 12 albidv 
 |-  ( k = 0 -> ( A. x ( S ( R ^r k ) x -> ps ) <-> A. x ( S ( R ^r 0 ) x -> ps ) ) )
14 9 13 imbi12d 
 |-  ( k = 0 -> ( ( ( ( et /\ R e. _V ) /\ k e. NN0 ) -> A. x ( S ( R ^r k ) x -> ps ) ) <-> ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> A. x ( S ( R ^r 0 ) x -> ps ) ) ) )
15 eleq1 
 |-  ( k = l -> ( k e. NN0 <-> l e. NN0 ) )
16 15 anbi2d 
 |-  ( k = l -> ( ( ( et /\ R e. _V ) /\ k e. NN0 ) <-> ( ( et /\ R e. _V ) /\ l e. NN0 ) ) )
17 oveq2 
 |-  ( k = l -> ( R ^r k ) = ( R ^r l ) )
18 17 breqd 
 |-  ( k = l -> ( S ( R ^r k ) x <-> S ( R ^r l ) x ) )
19 18 imbi1d 
 |-  ( k = l -> ( ( S ( R ^r k ) x -> ps ) <-> ( S ( R ^r l ) x -> ps ) ) )
20 19 albidv 
 |-  ( k = l -> ( A. x ( S ( R ^r k ) x -> ps ) <-> A. x ( S ( R ^r l ) x -> ps ) ) )
21 16 20 imbi12d 
 |-  ( k = l -> ( ( ( ( et /\ R e. _V ) /\ k e. NN0 ) -> A. x ( S ( R ^r k ) x -> ps ) ) <-> ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) ) )
22 eleq1 
 |-  ( k = ( l + 1 ) -> ( k e. NN0 <-> ( l + 1 ) e. NN0 ) )
23 22 anbi2d 
 |-  ( k = ( l + 1 ) -> ( ( ( et /\ R e. _V ) /\ k e. NN0 ) <-> ( ( et /\ R e. _V ) /\ ( l + 1 ) e. NN0 ) ) )
24 oveq2 
 |-  ( k = ( l + 1 ) -> ( R ^r k ) = ( R ^r ( l + 1 ) ) )
25 24 breqd 
 |-  ( k = ( l + 1 ) -> ( S ( R ^r k ) x <-> S ( R ^r ( l + 1 ) ) x ) )
26 25 imbi1d 
 |-  ( k = ( l + 1 ) -> ( ( S ( R ^r k ) x -> ps ) <-> ( S ( R ^r ( l + 1 ) ) x -> ps ) ) )
27 26 albidv 
 |-  ( k = ( l + 1 ) -> ( A. x ( S ( R ^r k ) x -> ps ) <-> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) ) )
28 23 27 imbi12d 
 |-  ( k = ( l + 1 ) -> ( ( ( ( et /\ R e. _V ) /\ k e. NN0 ) -> A. x ( S ( R ^r k ) x -> ps ) ) <-> ( ( ( et /\ R e. _V ) /\ ( l + 1 ) e. NN0 ) -> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) ) ) )
29 eleq1 
 |-  ( k = n -> ( k e. NN0 <-> n e. NN0 ) )
30 29 anbi2d 
 |-  ( k = n -> ( ( ( et /\ R e. _V ) /\ k e. NN0 ) <-> ( ( et /\ R e. _V ) /\ n e. NN0 ) ) )
31 oveq2 
 |-  ( k = n -> ( R ^r k ) = ( R ^r n ) )
32 31 breqd 
 |-  ( k = n -> ( S ( R ^r k ) x <-> S ( R ^r n ) x ) )
33 32 imbi1d 
 |-  ( k = n -> ( ( S ( R ^r k ) x -> ps ) <-> ( S ( R ^r n ) x -> ps ) ) )
34 33 albidv 
 |-  ( k = n -> ( A. x ( S ( R ^r k ) x -> ps ) <-> A. x ( S ( R ^r n ) x -> ps ) ) )
35 30 34 imbi12d 
 |-  ( k = n -> ( ( ( ( et /\ R e. _V ) /\ k e. NN0 ) -> A. x ( S ( R ^r k ) x -> ps ) ) <-> ( ( ( et /\ R e. _V ) /\ n e. NN0 ) -> A. x ( S ( R ^r n ) x -> ps ) ) ) )
36 1 anim1ci 
 |-  ( ( et /\ R e. _V ) -> ( R e. _V /\ Rel R ) )
37 36 adantr 
 |-  ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> ( R e. _V /\ Rel R ) )
38 relexp0 
 |-  ( ( R e. _V /\ Rel R ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
39 37 38 syl 
 |-  ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
40 6 adantr 
 |-  ( ( et /\ R e. _V ) -> ch )
41 simpl 
 |-  ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> ( et /\ R e. _V ) )
42 2 ad2antrl 
 |-  ( ( ch /\ ( et /\ R e. _V ) ) -> S e. V )
43 simprl 
 |-  ( ( i = S /\ ( ( et /\ R e. _V ) /\ ( ph /\ i = S ) ) ) -> ( et /\ R e. _V ) )
44 43 40 jccil 
 |-  ( ( i = S /\ ( ( et /\ R e. _V ) /\ ( ph /\ i = S ) ) ) -> ( ch /\ ( et /\ R e. _V ) ) )
45 44 expcom 
 |-  ( ( ( et /\ R e. _V ) /\ ( ph /\ i = S ) ) -> ( i = S -> ( ch /\ ( et /\ R e. _V ) ) ) )
46 45 expcom 
 |-  ( ( ph /\ i = S ) -> ( ( et /\ R e. _V ) -> ( i = S -> ( ch /\ ( et /\ R e. _V ) ) ) ) )
47 46 expcom 
 |-  ( i = S -> ( ph -> ( ( et /\ R e. _V ) -> ( i = S -> ( ch /\ ( et /\ R e. _V ) ) ) ) ) )
48 47 3imp1 
 |-  ( ( ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ i = S ) -> ( ch /\ ( et /\ R e. _V ) ) )
49 48 expcom 
 |-  ( i = S -> ( ( i = S /\ ph /\ ( et /\ R e. _V ) ) -> ( ch /\ ( et /\ R e. _V ) ) ) )
50 simprr 
 |-  ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> i = S )
51 3 ad2antll 
 |-  ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> ( ph <-> ch ) )
52 51 bicomd 
 |-  ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> ( ch <-> ph ) )
53 anbi1 
 |-  ( ( ch <-> ph ) -> ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) <-> ( ph /\ ( ( et /\ R e. _V ) /\ i = S ) ) ) )
54 simpl 
 |-  ( ( ph /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> ph )
55 53 54 syl6bi 
 |-  ( ( ch <-> ph ) -> ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> ph ) )
56 52 55 mpcom 
 |-  ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> ph )
57 simprl 
 |-  ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> ( et /\ R e. _V ) )
58 50 56 57 3jca 
 |-  ( ( ch /\ ( ( et /\ R e. _V ) /\ i = S ) ) -> ( i = S /\ ph /\ ( et /\ R e. _V ) ) )
59 58 anassrs 
 |-  ( ( ( ch /\ ( et /\ R e. _V ) ) /\ i = S ) -> ( i = S /\ ph /\ ( et /\ R e. _V ) ) )
60 59 expcom 
 |-  ( i = S -> ( ( ch /\ ( et /\ R e. _V ) ) -> ( i = S /\ ph /\ ( et /\ R e. _V ) ) ) )
61 49 60 impbid 
 |-  ( i = S -> ( ( i = S /\ ph /\ ( et /\ R e. _V ) ) <-> ( ch /\ ( et /\ R e. _V ) ) ) )
62 61 spcegv 
 |-  ( S e. V -> ( ( ch /\ ( et /\ R e. _V ) ) -> E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) ) )
63 42 62 mpcom 
 |-  ( ( ch /\ ( et /\ R e. _V ) ) -> E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) )
64 40 41 63 syl2an2r 
 |-  ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) )
65 simpl 
 |-  ( ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) -> S ( _I |` U. U. R ) x )
66 df-br 
 |-  ( S ( _I |` U. U. R ) x <-> <. S , x >. e. ( _I |` U. U. R ) )
67 65 66 sylib 
 |-  ( ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) -> <. S , x >. e. ( _I |` U. U. R ) )
68 vex 
 |-  x e. _V
69 68 opelresi 
 |-  ( <. S , x >. e. ( _I |` U. U. R ) <-> ( S e. U. U. R /\ <. S , x >. e. _I ) )
70 67 69 sylib 
 |-  ( ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) -> ( S e. U. U. R /\ <. S , x >. e. _I ) )
71 simplr 
 |-  ( ( ( S e. U. U. R /\ <. S , x >. e. _I ) /\ ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) ) -> <. S , x >. e. _I )
72 df-br 
 |-  ( S _I x <-> <. S , x >. e. _I )
73 71 72 sylibr 
 |-  ( ( ( S e. U. U. R /\ <. S , x >. e. _I ) /\ ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) ) -> S _I x )
74 68 ideq 
 |-  ( S _I x <-> S = x )
75 73 74 sylib 
 |-  ( ( ( S e. U. U. R /\ <. S , x >. e. _I ) /\ ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) ) -> S = x )
76 70 75 mpancom 
 |-  ( ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) -> S = x )
77 breq1 
 |-  ( S = x -> ( S ( _I |` U. U. R ) x <-> x ( _I |` U. U. R ) x ) )
78 eqeq2 
 |-  ( S = x -> ( i = S <-> i = x ) )
79 78 3anbi1d 
 |-  ( S = x -> ( ( i = S /\ ph /\ ( et /\ R e. _V ) ) <-> ( i = x /\ ph /\ ( et /\ R e. _V ) ) ) )
80 79 exbidv 
 |-  ( S = x -> ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) <-> E. i ( i = x /\ ph /\ ( et /\ R e. _V ) ) ) )
81 80 anbi1d 
 |-  ( S = x -> ( ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) <-> ( E. i ( i = x /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) )
82 77 81 anbi12d 
 |-  ( S = x -> ( ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) <-> ( x ( _I |` U. U. R ) x /\ ( E. i ( i = x /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) ) )
83 simprl 
 |-  ( ( ( et /\ R e. _V ) /\ ( ph /\ i = x ) ) -> ph )
84 4 ad2antll 
 |-  ( ( ( et /\ R e. _V ) /\ ( ph /\ i = x ) ) -> ( ph <-> ps ) )
85 83 84 mpbid 
 |-  ( ( ( et /\ R e. _V ) /\ ( ph /\ i = x ) ) -> ps )
86 85 expcom 
 |-  ( ( ph /\ i = x ) -> ( ( et /\ R e. _V ) -> ps ) )
87 86 expcom 
 |-  ( i = x -> ( ph -> ( ( et /\ R e. _V ) -> ps ) ) )
88 87 3imp 
 |-  ( ( i = x /\ ph /\ ( et /\ R e. _V ) ) -> ps )
89 88 exlimiv 
 |-  ( E. i ( i = x /\ ph /\ ( et /\ R e. _V ) ) -> ps )
90 89 ad2antrl 
 |-  ( ( x ( _I |` U. U. R ) x /\ ( E. i ( i = x /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) -> ps )
91 82 90 syl6bi 
 |-  ( S = x -> ( ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) -> ps ) )
92 76 91 mpcom 
 |-  ( ( S ( _I |` U. U. R ) x /\ ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) ) -> ps )
93 92 expcom 
 |-  ( ( E. i ( i = S /\ ph /\ ( et /\ R e. _V ) ) /\ ( ( et /\ R e. _V ) /\ 0 e. NN0 ) ) -> ( S ( _I |` U. U. R ) x -> ps ) )
94 64 93 mpancom 
 |-  ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> ( S ( _I |` U. U. R ) x -> ps ) )
95 breq 
 |-  ( ( R ^r 0 ) = ( _I |` U. U. R ) -> ( S ( R ^r 0 ) x <-> S ( _I |` U. U. R ) x ) )
96 95 imbi1d 
 |-  ( ( R ^r 0 ) = ( _I |` U. U. R ) -> ( ( S ( R ^r 0 ) x -> ps ) <-> ( S ( _I |` U. U. R ) x -> ps ) ) )
97 94 96 syl5ibr 
 |-  ( ( R ^r 0 ) = ( _I |` U. U. R ) -> ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> ( S ( R ^r 0 ) x -> ps ) ) )
98 39 97 mpcom 
 |-  ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> ( S ( R ^r 0 ) x -> ps ) )
99 98 alrimiv 
 |-  ( ( ( et /\ R e. _V ) /\ 0 e. NN0 ) -> A. x ( S ( R ^r 0 ) x -> ps ) )
100 breq2 
 |-  ( i = x -> ( S ( R ^r l ) i <-> S ( R ^r l ) x ) )
101 100 4 imbi12d 
 |-  ( i = x -> ( ( S ( R ^r l ) i -> ph ) <-> ( S ( R ^r l ) x -> ps ) ) )
102 101 cbvalvw 
 |-  ( A. i ( S ( R ^r l ) i -> ph ) <-> A. x ( S ( R ^r l ) x -> ps ) )
103 102 bicomi 
 |-  ( A. x ( S ( R ^r l ) x -> ps ) <-> A. i ( S ( R ^r l ) i -> ph ) )
104 imbi2 
 |-  ( ( A. x ( S ( R ^r l ) x -> ps ) <-> A. i ( S ( R ^r l ) i -> ph ) ) -> ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) <-> ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) ) )
105 104 anbi1d 
 |-  ( ( A. x ( S ( R ^r l ) x -> ps ) <-> A. i ( S ( R ^r l ) i -> ph ) ) -> ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) /\ l e. NN0 ) <-> ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) )
106 105 anbi2d 
 |-  ( ( A. x ( S ( R ^r l ) x -> ps ) <-> A. i ( S ( R ^r l ) i -> ph ) ) -> ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) /\ l e. NN0 ) ) <-> ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) )
107 106 anbi2d 
 |-  ( ( A. x ( S ( R ^r l ) x -> ps ) <-> A. i ( S ( R ^r l ) i -> ph ) ) -> ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) /\ l e. NN0 ) ) ) <-> ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) ) )
108 1 adantr 
 |-  ( ( et /\ R e. _V ) -> Rel R )
109 108 adantr 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) -> Rel R )
110 simprrr 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) -> l e. NN0 )
111 109 110 relexpsucld 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) -> ( R ^r ( l + 1 ) ) = ( R o. ( R ^r l ) ) )
112 simpl 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) ) -> S ( R o. ( R ^r l ) ) x )
113 2 adantr 
 |-  ( ( et /\ R e. _V ) -> S e. V )
114 113 ad2antrl 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) ) -> S e. V )
115 brcog 
 |-  ( ( S e. V /\ x e. _V ) -> ( S ( R o. ( R ^r l ) ) x <-> E. j ( S ( R ^r l ) j /\ j R x ) ) )
116 114 68 115 sylancl 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) ) -> ( S ( R o. ( R ^r l ) ) x <-> E. j ( S ( R ^r l ) j /\ j R x ) ) )
117 112 116 mpbid 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) ) -> E. j ( S ( R ^r l ) j /\ j R x ) )
118 simprl 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) -> ( et /\ R e. _V ) )
119 simprrl 
 |-  ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) -> l e. NN0 )
120 119 ad2antll 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) -> l e. NN0 )
121 simprl 
 |-  ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) -> ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) )
122 121 ad2antll 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) -> ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) )
123 118 120 122 mp2and 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) -> A. i ( S ( R ^r l ) i -> ph ) )
124 simprrl 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> ( et /\ R e. _V ) )
125 simprrr 
 |-  ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) -> j R x )
126 125 ad2antll 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) -> j R x )
127 126 ad2antll 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> j R x )
128 breq2 
 |-  ( i = j -> ( S ( R ^r l ) i <-> S ( R ^r l ) j ) )
129 128 5 imbi12d 
 |-  ( i = j -> ( ( S ( R ^r l ) i -> ph ) <-> ( S ( R ^r l ) j -> th ) ) )
130 129 cbvalvw 
 |-  ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) )
131 id 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) )
132 imbi2 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) <-> ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) ) )
133 132 anbi1d 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) <-> ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) )
134 133 anbi2d 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) <-> ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) )
135 134 anbi2d 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) <-> ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) )
136 135 anbi2d 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) <-> ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) )
137 131 136 anbi12d 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( ( A. i ( S ( R ^r l ) i -> ph ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) <-> ( A. j ( S ( R ^r l ) j -> th ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) ) )
138 simprrl 
 |-  ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) -> S ( R ^r l ) j )
139 138 ad2antll 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) -> S ( R ^r l ) j )
140 139 ad2antll 
 |-  ( ( A. j ( S ( R ^r l ) j -> th ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> S ( R ^r l ) j )
141 sp 
 |-  ( A. j ( S ( R ^r l ) j -> th ) -> ( S ( R ^r l ) j -> th ) )
142 141 adantr 
 |-  ( ( A. j ( S ( R ^r l ) j -> th ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> ( S ( R ^r l ) j -> th ) )
143 140 142 mpd 
 |-  ( ( A. j ( S ( R ^r l ) j -> th ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. j ( S ( R ^r l ) j -> th ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> th )
144 137 143 syl6bi 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) <-> A. j ( S ( R ^r l ) j -> th ) ) -> ( ( A. i ( S ( R ^r l ) i -> ph ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> th ) )
145 130 144 ax-mp 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> th )
146 7 adantr 
 |-  ( ( et /\ R e. _V ) -> ( j R x -> ( th -> ps ) ) )
147 124 127 145 146 syl3c 
 |-  ( ( A. i ( S ( R ^r l ) i -> ph ) /\ ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) ) -> ps )
148 123 147 mpancom 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) ) -> ps )
149 148 expcom 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) )
150 149 expcom 
 |-  ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) ) -> ( ( et /\ R e. _V ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) ) )
151 150 expcom 
 |-  ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ ( l e. NN0 /\ ( S ( R ^r l ) j /\ j R x ) ) ) -> ( ( l + 1 ) e. NN0 -> ( ( et /\ R e. _V ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) ) ) )
152 151 anassrs 
 |-  ( ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) /\ ( S ( R ^r l ) j /\ j R x ) ) -> ( ( l + 1 ) e. NN0 -> ( ( et /\ R e. _V ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) ) ) )
153 152 impcom 
 |-  ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) /\ ( S ( R ^r l ) j /\ j R x ) ) ) -> ( ( et /\ R e. _V ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) ) )
154 153 anassrs 
 |-  ( ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) /\ ( S ( R ^r l ) j /\ j R x ) ) -> ( ( et /\ R e. _V ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) ) )
155 154 impcom 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) /\ ( S ( R ^r l ) j /\ j R x ) ) ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) )
156 155 anassrs 
 |-  ( ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) /\ ( S ( R ^r l ) j /\ j R x ) ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) )
157 156 impcom 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) /\ ( S ( R ^r l ) j /\ j R x ) ) ) -> ps )
158 157 anassrs 
 |-  ( ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) ) /\ ( S ( R ^r l ) j /\ j R x ) ) -> ps )
159 117 158 exlimddv 
 |-  ( ( S ( R o. ( R ^r l ) ) x /\ ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) ) -> ps )
160 159 expcom 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) -> ( S ( R o. ( R ^r l ) ) x -> ps ) )
161 breq 
 |-  ( ( R ^r ( l + 1 ) ) = ( R o. ( R ^r l ) ) -> ( S ( R ^r ( l + 1 ) ) x <-> S ( R o. ( R ^r l ) ) x ) )
162 161 imbi1d 
 |-  ( ( R ^r ( l + 1 ) ) = ( R o. ( R ^r l ) ) -> ( ( S ( R ^r ( l + 1 ) ) x -> ps ) <-> ( S ( R o. ( R ^r l ) ) x -> ps ) ) )
163 160 162 syl5ibr 
 |-  ( ( R ^r ( l + 1 ) ) = ( R o. ( R ^r l ) ) -> ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) -> ( S ( R ^r ( l + 1 ) ) x -> ps ) ) )
164 111 163 mpcom 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) -> ( S ( R ^r ( l + 1 ) ) x -> ps ) )
165 164 alrimiv 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. i ( S ( R ^r l ) i -> ph ) ) /\ l e. NN0 ) ) ) -> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) )
166 107 165 syl6bi 
 |-  ( ( A. x ( S ( R ^r l ) x -> ps ) <-> A. i ( S ( R ^r l ) i -> ph ) ) -> ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) /\ l e. NN0 ) ) ) -> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) ) )
167 103 166 ax-mp 
 |-  ( ( ( et /\ R e. _V ) /\ ( ( l + 1 ) e. NN0 /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) /\ l e. NN0 ) ) ) -> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) )
168 167 anassrs 
 |-  ( ( ( ( et /\ R e. _V ) /\ ( l + 1 ) e. NN0 ) /\ ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) /\ l e. NN0 ) ) -> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) )
169 168 expcom 
 |-  ( ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) /\ l e. NN0 ) -> ( ( ( et /\ R e. _V ) /\ ( l + 1 ) e. NN0 ) -> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) ) )
170 169 expcom 
 |-  ( l e. NN0 -> ( ( ( ( et /\ R e. _V ) /\ l e. NN0 ) -> A. x ( S ( R ^r l ) x -> ps ) ) -> ( ( ( et /\ R e. _V ) /\ ( l + 1 ) e. NN0 ) -> A. x ( S ( R ^r ( l + 1 ) ) x -> ps ) ) ) )
171 14 21 28 35 99 170 nn0ind 
 |-  ( n e. NN0 -> ( ( ( et /\ R e. _V ) /\ n e. NN0 ) -> A. x ( S ( R ^r n ) x -> ps ) ) )
172 171 anabsi7 
 |-  ( ( ( et /\ R e. _V ) /\ n e. NN0 ) -> A. x ( S ( R ^r n ) x -> ps ) )
173 172 19.21bi 
 |-  ( ( ( et /\ R e. _V ) /\ n e. NN0 ) -> ( S ( R ^r n ) x -> ps ) )
174 173 exp31 
 |-  ( et -> ( R e. _V -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) ) )
175 reldmrelexp 
 |-  Rel dom ^r
176 175 ovprc1 
 |-  ( -. R e. _V -> ( R ^r n ) = (/) )
177 176 breqd 
 |-  ( -. R e. _V -> ( S ( R ^r n ) x <-> S (/) x ) )
178 br0 
 |-  -. S (/) x
179 178 pm2.21i 
 |-  ( S (/) x -> ps )
180 177 179 syl6bi 
 |-  ( -. R e. _V -> ( S ( R ^r n ) x -> ps ) )
181 180 a1d 
 |-  ( -. R e. _V -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) )
182 174 181 pm2.61d1 
 |-  ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) )