This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem aomclem8

Description: Lemma for dfac11 . Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem8.a 
|- ( ph -> A e. On )
aomclem8.y 
|- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
Assertion aomclem8 
|- ( ph -> E. b b We ( R1 ` A ) )

Proof

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 ) )