Step |
Hyp |
Ref |
Expression |
1 |
|
aomclem8.a |
|- ( ph -> A e. On ) |
2 |
|
aomclem8.y |
|- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) ) |
3 |
|
elequ2 |
|- ( h = b -> ( i e. h <-> i e. b ) ) |
4 |
|
elequ2 |
|- ( g = c -> ( i e. g <-> i e. c ) ) |
5 |
4
|
notbid |
|- ( g = c -> ( -. i e. g <-> -. i e. c ) ) |
6 |
3 5
|
bi2anan9r |
|- ( ( g = c /\ h = b ) -> ( ( i e. h /\ -. i e. g ) <-> ( i e. b /\ -. i e. c ) ) ) |
7 |
|
elequ2 |
|- ( g = c -> ( j e. g <-> j e. c ) ) |
8 |
|
elequ2 |
|- ( h = b -> ( j e. h <-> j e. b ) ) |
9 |
7 8
|
bi2bian9 |
|- ( ( g = c /\ h = b ) -> ( ( j e. g <-> j e. h ) <-> ( j e. c <-> j e. b ) ) ) |
10 |
9
|
imbi2d |
|- ( ( g = c /\ h = b ) -> ( ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) <-> ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) ) ) |
11 |
10
|
ralbidv |
|- ( ( g = c /\ h = b ) -> ( A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) <-> A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) ) ) |
12 |
6 11
|
anbi12d |
|- ( ( g = c /\ h = b ) -> ( ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) <-> ( ( i e. b /\ -. i e. c ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) ) ) ) |
13 |
12
|
rexbidv |
|- ( ( g = c /\ h = b ) -> ( E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) <-> E. i e. ( R1 ` U. dom e ) ( ( i e. b /\ -. i e. c ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) ) ) ) |
14 |
|
elequ1 |
|- ( i = d -> ( i e. b <-> d e. b ) ) |
15 |
|
elequ1 |
|- ( i = d -> ( i e. c <-> d e. c ) ) |
16 |
15
|
notbid |
|- ( i = d -> ( -. i e. c <-> -. d e. c ) ) |
17 |
14 16
|
anbi12d |
|- ( i = d -> ( ( i e. b /\ -. i e. c ) <-> ( d e. b /\ -. d e. c ) ) ) |
18 |
|
breq2 |
|- ( i = d -> ( j ( e ` U. dom e ) i <-> j ( e ` U. dom e ) d ) ) |
19 |
18
|
imbi1d |
|- ( i = d -> ( ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) <-> ( j ( e ` U. dom e ) d -> ( j e. c <-> j e. b ) ) ) ) |
20 |
19
|
ralbidv |
|- ( i = d -> ( A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) <-> A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) d -> ( j e. c <-> j e. b ) ) ) ) |
21 |
|
breq1 |
|- ( j = f -> ( j ( e ` U. dom e ) d <-> f ( e ` U. dom e ) d ) ) |
22 |
|
elequ1 |
|- ( j = f -> ( j e. c <-> f e. c ) ) |
23 |
|
elequ1 |
|- ( j = f -> ( j e. b <-> f e. b ) ) |
24 |
22 23
|
bibi12d |
|- ( j = f -> ( ( j e. c <-> j e. b ) <-> ( f e. c <-> f e. b ) ) ) |
25 |
21 24
|
imbi12d |
|- ( j = f -> ( ( j ( e ` U. dom e ) d -> ( j e. c <-> j e. b ) ) <-> ( f ( e ` U. dom e ) d -> ( f e. c <-> f e. b ) ) ) ) |
26 |
25
|
cbvralvw |
|- ( A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) d -> ( j e. c <-> j e. b ) ) <-> A. f e. ( R1 ` U. dom e ) ( f ( e ` U. dom e ) d -> ( f e. c <-> f e. b ) ) ) |
27 |
20 26
|
bitrdi |
|- ( i = d -> ( A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) <-> A. f e. ( R1 ` U. dom e ) ( f ( e ` U. dom e ) d -> ( f e. c <-> f e. b ) ) ) ) |
28 |
17 27
|
anbi12d |
|- ( i = d -> ( ( ( i e. b /\ -. i e. c ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) ) <-> ( ( d e. b /\ -. d e. c ) /\ A. f e. ( R1 ` U. dom e ) ( f ( e ` U. dom e ) d -> ( f e. c <-> f e. b ) ) ) ) ) |
29 |
28
|
cbvrexvw |
|- ( E. i e. ( R1 ` U. dom e ) ( ( i e. b /\ -. i e. c ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. c <-> j e. b ) ) ) <-> E. d e. ( R1 ` U. dom e ) ( ( d e. b /\ -. d e. c ) /\ A. f e. ( R1 ` U. dom e ) ( f ( e ` U. dom e ) d -> ( f e. c <-> f e. b ) ) ) ) |
30 |
13 29
|
bitrdi |
|- ( ( g = c /\ h = b ) -> ( E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) <-> E. d e. ( R1 ` U. dom e ) ( ( d e. b /\ -. d e. c ) /\ A. f e. ( R1 ` U. dom e ) ( f ( e ` U. dom e ) d -> ( f e. c <-> f e. b ) ) ) ) ) |
31 |
30
|
cbvopabv |
|- { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } = { <. c , b >. | E. d e. ( R1 ` U. dom e ) ( ( d e. b /\ -. d e. c ) /\ A. f e. ( R1 ` U. dom e ) ( f ( e ` U. dom e ) d -> ( f e. c <-> f e. b ) ) ) } |
32 |
|
nfcv |
|- F/_ c sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) |
33 |
|
nfcv |
|- F/_ g ( y ` c ) |
34 |
|
nfcv |
|- F/_ g ( R1 ` dom e ) |
35 |
|
nfopab1 |
|- F/_ g { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } |
36 |
33 34 35
|
nfsup |
|- F/_ g sup ( ( y ` c ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) |
37 |
|
fveq2 |
|- ( g = c -> ( y ` g ) = ( y ` c ) ) |
38 |
37
|
supeq1d |
|- ( g = c -> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) = sup ( ( y ` c ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) |
39 |
32 36 38
|
cbvmpt |
|- ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) = ( c e. _V |-> sup ( ( y ` c ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) |
40 |
|
nfcv |
|- F/_ c ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) |
41 |
|
nffvmpt1 |
|- F/_ g ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran c ) ) |
42 |
|
rneq |
|- ( g = c -> ran g = ran c ) |
43 |
42
|
difeq2d |
|- ( g = c -> ( ( R1 ` dom e ) \ ran g ) = ( ( R1 ` dom e ) \ ran c ) ) |
44 |
43
|
fveq2d |
|- ( g = c -> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) = ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran c ) ) ) |
45 |
40 41 44
|
cbvmpt |
|- ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) = ( c e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran c ) ) ) |
46 |
|
recseq |
|- ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) = ( c e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran c ) ) ) -> recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) = recs ( ( c e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran c ) ) ) ) ) |
47 |
45 46
|
ax-mp |
|- recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) = recs ( ( c e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran c ) ) ) ) |
48 |
|
nfv |
|- F/ c |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) |
49 |
|
nfv |
|- F/ b |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) |
50 |
|
nfmpt1 |
|- F/_ g ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) |
51 |
50
|
nfrecs |
|- F/_ g recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) |
52 |
51
|
nfcnv |
|- F/_ g `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) |
53 |
|
nfcv |
|- F/_ g { c } |
54 |
52 53
|
nfima |
|- F/_ g ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) |
55 |
54
|
nfint |
|- F/_ g |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) |
56 |
|
nfcv |
|- F/_ g { b } |
57 |
52 56
|
nfima |
|- F/_ g ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) |
58 |
57
|
nfint |
|- F/_ g |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) |
59 |
55 58
|
nfel |
|- F/ g |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) |
60 |
|
nfcv |
|- F/_ h _V |
61 |
|
nfcv |
|- F/_ h ( y ` g ) |
62 |
|
nfcv |
|- F/_ h ( R1 ` dom e ) |
63 |
|
nfopab2 |
|- F/_ h { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } |
64 |
61 62 63
|
nfsup |
|- F/_ h sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) |
65 |
60 64
|
nfmpt |
|- F/_ h ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) |
66 |
|
nfcv |
|- F/_ h ( ( R1 ` dom e ) \ ran g ) |
67 |
65 66
|
nffv |
|- F/_ h ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) |
68 |
60 67
|
nfmpt |
|- F/_ h ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) |
69 |
68
|
nfrecs |
|- F/_ h recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) |
70 |
69
|
nfcnv |
|- F/_ h `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) |
71 |
|
nfcv |
|- F/_ h { c } |
72 |
70 71
|
nfima |
|- F/_ h ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) |
73 |
72
|
nfint |
|- F/_ h |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) |
74 |
|
nfcv |
|- F/_ h { b } |
75 |
70 74
|
nfima |
|- F/_ h ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) |
76 |
75
|
nfint |
|- F/_ h |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) |
77 |
73 76
|
nfel |
|- F/ h |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) |
78 |
|
sneq |
|- ( g = c -> { g } = { c } ) |
79 |
78
|
imaeq2d |
|- ( g = c -> ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) = ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) ) |
80 |
79
|
inteqd |
|- ( g = c -> |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) = |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) ) |
81 |
|
sneq |
|- ( h = b -> { h } = { b } ) |
82 |
81
|
imaeq2d |
|- ( h = b -> ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) = ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) ) |
83 |
82
|
inteqd |
|- ( h = b -> |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) = |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) ) |
84 |
|
eleq12 |
|- ( ( |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) = |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) /\ |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) = |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) ) -> ( |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) <-> |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) ) ) |
85 |
80 83 84
|
syl2an |
|- ( ( g = c /\ h = b ) -> ( |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) <-> |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) ) ) |
86 |
48 49 59 77 85
|
cbvopab |
|- { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } = { <. c , b >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { c } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { b } ) } |
87 |
|
fveq2 |
|- ( g = c -> ( rank ` g ) = ( rank ` c ) ) |
88 |
|
fveq2 |
|- ( h = b -> ( rank ` h ) = ( rank ` b ) ) |
89 |
87 88
|
breqan12d |
|- ( ( g = c /\ h = b ) -> ( ( rank ` g ) _E ( rank ` h ) <-> ( rank ` c ) _E ( rank ` b ) ) ) |
90 |
87 88
|
eqeqan12d |
|- ( ( g = c /\ h = b ) -> ( ( rank ` g ) = ( rank ` h ) <-> ( rank ` c ) = ( rank ` b ) ) ) |
91 |
|
simpl |
|- ( ( g = c /\ h = b ) -> g = c ) |
92 |
|
suceq |
|- ( ( rank ` g ) = ( rank ` c ) -> suc ( rank ` g ) = suc ( rank ` c ) ) |
93 |
87 92
|
syl |
|- ( g = c -> suc ( rank ` g ) = suc ( rank ` c ) ) |
94 |
93
|
adantr |
|- ( ( g = c /\ h = b ) -> suc ( rank ` g ) = suc ( rank ` c ) ) |
95 |
94
|
fveq2d |
|- ( ( g = c /\ h = b ) -> ( e ` suc ( rank ` g ) ) = ( e ` suc ( rank ` c ) ) ) |
96 |
|
simpr |
|- ( ( g = c /\ h = b ) -> h = b ) |
97 |
91 95 96
|
breq123d |
|- ( ( g = c /\ h = b ) -> ( g ( e ` suc ( rank ` g ) ) h <-> c ( e ` suc ( rank ` c ) ) b ) ) |
98 |
90 97
|
anbi12d |
|- ( ( g = c /\ h = b ) -> ( ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) <-> ( ( rank ` c ) = ( rank ` b ) /\ c ( e ` suc ( rank ` c ) ) b ) ) ) |
99 |
89 98
|
orbi12d |
|- ( ( g = c /\ h = b ) -> ( ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) <-> ( ( rank ` c ) _E ( rank ` b ) \/ ( ( rank ` c ) = ( rank ` b ) /\ c ( e ` suc ( rank ` c ) ) b ) ) ) ) |
100 |
99
|
cbvopabv |
|- { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } = { <. c , b >. | ( ( rank ` c ) _E ( rank ` b ) \/ ( ( rank ` c ) = ( rank ` b ) /\ c ( e ` suc ( rank ` c ) ) b ) ) } |
101 |
|
eqid |
|- ( if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) = ( if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) |
102 |
|
dmeq |
|- ( l = e -> dom l = dom e ) |
103 |
102
|
unieqd |
|- ( l = e -> U. dom l = U. dom e ) |
104 |
102 103
|
eqeq12d |
|- ( l = e -> ( dom l = U. dom l <-> dom e = U. dom e ) ) |
105 |
|
fveq1 |
|- ( l = e -> ( l ` suc ( rank ` g ) ) = ( e ` suc ( rank ` g ) ) ) |
106 |
105
|
breqd |
|- ( l = e -> ( g ( l ` suc ( rank ` g ) ) h <-> g ( e ` suc ( rank ` g ) ) h ) ) |
107 |
106
|
anbi2d |
|- ( l = e -> ( ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) <-> ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) ) |
108 |
107
|
orbi2d |
|- ( l = e -> ( ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) <-> ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) ) ) |
109 |
108
|
opabbidv |
|- ( l = e -> { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) } = { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } ) |
110 |
|
eqidd |
|- ( l = e -> ( y ` g ) = ( y ` g ) ) |
111 |
102
|
fveq2d |
|- ( l = e -> ( R1 ` dom l ) = ( R1 ` dom e ) ) |
112 |
103
|
fveq2d |
|- ( l = e -> ( R1 ` U. dom l ) = ( R1 ` U. dom e ) ) |
113 |
|
id |
|- ( l = e -> l = e ) |
114 |
113 103
|
fveq12d |
|- ( l = e -> ( l ` U. dom l ) = ( e ` U. dom e ) ) |
115 |
114
|
breqd |
|- ( l = e -> ( j ( l ` U. dom l ) i <-> j ( e ` U. dom e ) i ) ) |
116 |
115
|
imbi1d |
|- ( l = e -> ( ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) <-> ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) ) |
117 |
112 116
|
raleqbidv |
|- ( l = e -> ( A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) <-> A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) ) |
118 |
117
|
anbi2d |
|- ( l = e -> ( ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) <-> ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) ) ) |
119 |
112 118
|
rexeqbidv |
|- ( l = e -> ( E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) <-> E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) ) ) |
120 |
119
|
opabbidv |
|- ( l = e -> { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } = { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) |
121 |
110 111 120
|
supeq123d |
|- ( l = e -> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) = sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) |
122 |
121
|
mpteq2dv |
|- ( l = e -> ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) = ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ) |
123 |
111
|
difeq1d |
|- ( l = e -> ( ( R1 ` dom l ) \ ran g ) = ( ( R1 ` dom e ) \ ran g ) ) |
124 |
122 123
|
fveq12d |
|- ( l = e -> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) = ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) |
125 |
124
|
mpteq2dv |
|- ( l = e -> ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) = ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) |
126 |
|
recseq |
|- ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) = ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) -> recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) = recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) ) |
127 |
125 126
|
syl |
|- ( l = e -> recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) = recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) ) |
128 |
127
|
cnveqd |
|- ( l = e -> `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) = `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) ) |
129 |
128
|
imaeq1d |
|- ( l = e -> ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) = ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) ) |
130 |
129
|
inteqd |
|- ( l = e -> |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) = |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) ) |
131 |
128
|
imaeq1d |
|- ( l = e -> ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) = ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) ) |
132 |
131
|
inteqd |
|- ( l = e -> |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) = |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) ) |
133 |
130 132
|
eleq12d |
|- ( l = e -> ( |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) <-> |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) ) ) |
134 |
133
|
opabbidv |
|- ( l = e -> { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) } = { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) |
135 |
104 109 134
|
ifbieq12d |
|- ( l = e -> if ( dom l = U. dom l , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) } ) = if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) ) |
136 |
111
|
sqxpeqd |
|- ( l = e -> ( ( R1 ` dom l ) X. ( R1 ` dom l ) ) = ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) |
137 |
135 136
|
ineq12d |
|- ( l = e -> ( if ( dom l = U. dom l , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom l ) X. ( R1 ` dom l ) ) ) = ( if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) ) |
138 |
137
|
cbvmptv |
|- ( l e. _V |-> ( if ( dom l = U. dom l , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom l ) X. ( R1 ` dom l ) ) ) ) = ( e e. _V |-> ( if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) ) |
139 |
|
recseq |
|- ( ( l e. _V |-> ( if ( dom l = U. dom l , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom l ) X. ( R1 ` dom l ) ) ) ) = ( e e. _V |-> ( if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) ) -> recs ( ( l e. _V |-> ( if ( dom l = U. dom l , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom l ) X. ( R1 ` dom l ) ) ) ) ) = recs ( ( e e. _V |-> ( if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) ) ) ) |
140 |
138 139
|
ax-mp |
|- recs ( ( l e. _V |-> ( if ( dom l = U. dom l , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( l ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom l ) , { <. g , h >. | E. i e. ( R1 ` U. dom l ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom l ) ( j ( l ` U. dom l ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom l ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom l ) X. ( R1 ` dom l ) ) ) ) ) = recs ( ( e e. _V |-> ( if ( dom e = U. dom e , { <. g , h >. | ( ( rank ` g ) _E ( rank ` h ) \/ ( ( rank ` g ) = ( rank ` h ) /\ g ( e ` suc ( rank ` g ) ) h ) ) } , { <. g , h >. | |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { g } ) e. |^| ( `' recs ( ( g e. _V |-> ( ( g e. _V |-> sup ( ( y ` g ) , ( R1 ` dom e ) , { <. g , h >. | E. i e. ( R1 ` U. dom e ) ( ( i e. h /\ -. i e. g ) /\ A. j e. ( R1 ` U. dom e ) ( j ( e ` U. dom e ) i -> ( j e. g <-> j e. h ) ) ) } ) ) ` ( ( R1 ` dom e ) \ ran g ) ) ) ) " { h } ) } ) i^i ( ( R1 ` dom e ) X. ( R1 ` dom e ) ) ) ) ) |
141 |
|
neeq1 |
|- ( a = c -> ( a =/= (/) <-> c =/= (/) ) ) |
142 |
|
fveq2 |
|- ( a = c -> ( y ` a ) = ( y ` c ) ) |
143 |
|
pweq |
|- ( a = c -> ~P a = ~P c ) |
144 |
143
|
ineq1d |
|- ( a = c -> ( ~P a i^i Fin ) = ( ~P c i^i Fin ) ) |
145 |
144
|
difeq1d |
|- ( a = c -> ( ( ~P a i^i Fin ) \ { (/) } ) = ( ( ~P c i^i Fin ) \ { (/) } ) ) |
146 |
142 145
|
eleq12d |
|- ( a = c -> ( ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) <-> ( y ` c ) e. ( ( ~P c i^i Fin ) \ { (/) } ) ) ) |
147 |
141 146
|
imbi12d |
|- ( a = c -> ( ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) <-> ( c =/= (/) -> ( y ` c ) e. ( ( ~P c i^i Fin ) \ { (/) } ) ) ) ) |
148 |
147
|
cbvralvw |
|- ( A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) <-> A. c e. ~P ( R1 ` A ) ( c =/= (/) -> ( y ` c ) e. ( ( ~P c i^i Fin ) \ { (/) } ) ) ) |
149 |
2 148
|
sylib |
|- ( ph -> A. c e. ~P ( R1 ` A ) ( c =/= (/) -> ( y ` c ) e. ( ( ~P c i^i Fin ) \ { (/) } ) ) ) |
150 |
31 39 47 86 100 101 140 1 149
|
aomclem7 |
|- ( ph -> E. b b We ( R1 ` A ) ) |