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

Metamath Proof Explorer

Theorem ttrclselem2

Description: Lemma for ttrclse . Show that a suc N element long chain gives membership in the N -th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024)

Ref Expression
Hypothesis ttrclselem.1 
|- F = rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) )
Assertion ttrclselem2 
|- ( ( N e. _om /\ R Se A /\ X e. A ) -> ( E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` N ) ) )

Proof

Step Hyp Ref Expression
1 ttrclselem.1 
 |-  F = rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) )
2 suceq 
 |-  ( m = (/) -> suc m = suc (/) )
3 df-1o 
 |-  1o = suc (/)
4 2 3 eqtr4di 
 |-  ( m = (/) -> suc m = 1o )
5 suceq 
 |-  ( suc m = 1o -> suc suc m = suc 1o )
6 4 5 syl 
 |-  ( m = (/) -> suc suc m = suc 1o )
7 6 fneq2d 
 |-  ( m = (/) -> ( f Fn suc suc m <-> f Fn suc 1o ) )
8 4 fveqeq2d 
 |-  ( m = (/) -> ( ( f ` suc m ) = X <-> ( f ` 1o ) = X ) )
9 8 anbi2d 
 |-  ( m = (/) -> ( ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) <-> ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) )
10 df1o2 
 |-  1o = { (/) }
11 4 10 eqtrdi 
 |-  ( m = (/) -> suc m = { (/) } )
12 11 raleqdv 
 |-  ( m = (/) -> ( A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) <-> A. a e. { (/) } ( f ` a ) ( R |` A ) ( f ` suc a ) ) )
13 0ex 
 |-  (/) e. _V
14 fveq2 
 |-  ( a = (/) -> ( f ` a ) = ( f ` (/) ) )
15 suceq 
 |-  ( a = (/) -> suc a = suc (/) )
16 15 3 eqtr4di 
 |-  ( a = (/) -> suc a = 1o )
17 16 fveq2d 
 |-  ( a = (/) -> ( f ` suc a ) = ( f ` 1o ) )
18 14 17 breq12d 
 |-  ( a = (/) -> ( ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) )
19 13 18 ralsn 
 |-  ( A. a e. { (/) } ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` (/) ) ( R |` A ) ( f ` 1o ) )
20 12 19 bitrdi 
 |-  ( m = (/) -> ( A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) )
21 7 9 20 3anbi123d 
 |-  ( m = (/) -> ( ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) ) )
22 21 exbidv 
 |-  ( m = (/) -> ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) ) )
23 fveq2 
 |-  ( m = (/) -> ( F ` m ) = ( F ` (/) ) )
24 23 eleq2d 
 |-  ( m = (/) -> ( y e. ( F ` m ) <-> y e. ( F ` (/) ) ) )
25 22 24 bibi12d 
 |-  ( m = (/) -> ( ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> y e. ( F ` (/) ) ) ) )
26 25 albidv 
 |-  ( m = (/) -> ( A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> A. y ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> y e. ( F ` (/) ) ) ) )
27 26 imbi2d 
 |-  ( m = (/) -> ( ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) ) <-> ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> y e. ( F ` (/) ) ) ) ) )
28 suceq 
 |-  ( m = n -> suc m = suc n )
29 suceq 
 |-  ( suc m = suc n -> suc suc m = suc suc n )
30 28 29 syl 
 |-  ( m = n -> suc suc m = suc suc n )
31 30 fneq2d 
 |-  ( m = n -> ( f Fn suc suc m <-> f Fn suc suc n ) )
32 28 fveqeq2d 
 |-  ( m = n -> ( ( f ` suc m ) = X <-> ( f ` suc n ) = X ) )
33 32 anbi2d 
 |-  ( m = n -> ( ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) <-> ( ( f ` (/) ) = y /\ ( f ` suc n ) = X ) ) )
34 28 raleqdv 
 |-  ( m = n -> ( A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) <-> A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) )
35 fveq2 
 |-  ( a = c -> ( f ` a ) = ( f ` c ) )
36 suceq 
 |-  ( a = c -> suc a = suc c )
37 36 fveq2d 
 |-  ( a = c -> ( f ` suc a ) = ( f ` suc c ) )
38 35 37 breq12d 
 |-  ( a = c -> ( ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` c ) ( R |` A ) ( f ` suc c ) ) )
39 38 cbvralvw 
 |-  ( A. a e. suc n ( f ` a ) ( R |` A ) ( f ` suc a ) <-> A. c e. suc n ( f ` c ) ( R |` A ) ( f ` suc c ) )
40 34 39 bitrdi 
 |-  ( m = n -> ( A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) <-> A. c e. suc n ( f ` c ) ( R |` A ) ( f ` suc c ) ) )
41 31 33 40 3anbi123d 
 |-  ( m = n -> ( ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = X ) /\ A. c e. suc n ( f ` c ) ( R |` A ) ( f ` suc c ) ) ) )
42 41 exbidv 
 |-  ( m = n -> ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = X ) /\ A. c e. suc n ( f ` c ) ( R |` A ) ( f ` suc c ) ) ) )
43 fneq1 
 |-  ( f = g -> ( f Fn suc suc n <-> g Fn suc suc n ) )
44 fveq1 
 |-  ( f = g -> ( f ` (/) ) = ( g ` (/) ) )
45 44 eqeq1d 
 |-  ( f = g -> ( ( f ` (/) ) = y <-> ( g ` (/) ) = y ) )
46 fveq1 
 |-  ( f = g -> ( f ` suc n ) = ( g ` suc n ) )
47 46 eqeq1d 
 |-  ( f = g -> ( ( f ` suc n ) = X <-> ( g ` suc n ) = X ) )
48 45 47 anbi12d 
 |-  ( f = g -> ( ( ( f ` (/) ) = y /\ ( f ` suc n ) = X ) <-> ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) ) )
49 fveq1 
 |-  ( f = g -> ( f ` c ) = ( g ` c ) )
50 fveq1 
 |-  ( f = g -> ( f ` suc c ) = ( g ` suc c ) )
51 49 50 breq12d 
 |-  ( f = g -> ( ( f ` c ) ( R |` A ) ( f ` suc c ) <-> ( g ` c ) ( R |` A ) ( g ` suc c ) ) )
52 51 ralbidv 
 |-  ( f = g -> ( A. c e. suc n ( f ` c ) ( R |` A ) ( f ` suc c ) <-> A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) )
53 43 48 52 3anbi123d 
 |-  ( f = g -> ( ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = X ) /\ A. c e. suc n ( f ` c ) ( R |` A ) ( f ` suc c ) ) <-> ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
54 53 cbvexvw 
 |-  ( E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc n ) = X ) /\ A. c e. suc n ( f ` c ) ( R |` A ) ( f ` suc c ) ) <-> E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) )
55 42 54 bitrdi 
 |-  ( m = n -> ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
56 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
57 56 eleq2d 
 |-  ( m = n -> ( y e. ( F ` m ) <-> y e. ( F ` n ) ) )
58 55 57 bibi12d 
 |-  ( m = n -> ( ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> y e. ( F ` n ) ) ) )
59 58 albidv 
 |-  ( m = n -> ( A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> A. y ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> y e. ( F ` n ) ) ) )
60 eqeq2 
 |-  ( y = z -> ( ( g ` (/) ) = y <-> ( g ` (/) ) = z ) )
61 60 anbi1d 
 |-  ( y = z -> ( ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) <-> ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) ) )
62 61 3anbi2d 
 |-  ( y = z -> ( ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
63 62 exbidv 
 |-  ( y = z -> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
64 eleq1 
 |-  ( y = z -> ( y e. ( F ` n ) <-> z e. ( F ` n ) ) )
65 63 64 bibi12d 
 |-  ( y = z -> ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> y e. ( F ` n ) ) <-> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) )
66 65 cbvalvw 
 |-  ( A. y ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = y /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> y e. ( F ` n ) ) <-> A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) )
67 59 66 bitrdi 
 |-  ( m = n -> ( A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) )
68 67 imbi2d 
 |-  ( m = n -> ( ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) ) <-> ( ( R Se A /\ X e. A ) -> A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) ) )
69 suceq 
 |-  ( m = suc n -> suc m = suc suc n )
70 suceq 
 |-  ( suc m = suc suc n -> suc suc m = suc suc suc n )
71 69 70 syl 
 |-  ( m = suc n -> suc suc m = suc suc suc n )
72 71 fneq2d 
 |-  ( m = suc n -> ( f Fn suc suc m <-> f Fn suc suc suc n ) )
73 69 fveqeq2d 
 |-  ( m = suc n -> ( ( f ` suc m ) = X <-> ( f ` suc suc n ) = X ) )
74 73 anbi2d 
 |-  ( m = suc n -> ( ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) <-> ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) ) )
75 69 raleqdv 
 |-  ( m = suc n -> ( A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) <-> A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) )
76 72 74 75 3anbi123d 
 |-  ( m = suc n -> ( ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
77 76 exbidv 
 |-  ( m = suc n -> ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
78 fveq2 
 |-  ( m = suc n -> ( F ` m ) = ( F ` suc n ) )
79 78 eleq2d 
 |-  ( m = suc n -> ( y e. ( F ` m ) <-> y e. ( F ` suc n ) ) )
80 77 79 bibi12d 
 |-  ( m = suc n -> ( ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` suc n ) ) ) )
81 80 albidv 
 |-  ( m = suc n -> ( A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> A. y ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` suc n ) ) ) )
82 81 imbi2d 
 |-  ( m = suc n -> ( ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) ) <-> ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` suc n ) ) ) ) )
83 suceq 
 |-  ( m = N -> suc m = suc N )
84 suceq 
 |-  ( suc m = suc N -> suc suc m = suc suc N )
85 83 84 syl 
 |-  ( m = N -> suc suc m = suc suc N )
86 85 fneq2d 
 |-  ( m = N -> ( f Fn suc suc m <-> f Fn suc suc N ) )
87 83 fveqeq2d 
 |-  ( m = N -> ( ( f ` suc m ) = X <-> ( f ` suc N ) = X ) )
88 87 anbi2d 
 |-  ( m = N -> ( ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) <-> ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) ) )
89 83 raleqdv 
 |-  ( m = N -> ( A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) <-> A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) )
90 86 88 89 3anbi123d 
 |-  ( m = N -> ( ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
91 90 exbidv 
 |-  ( m = N -> ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
92 fveq2 
 |-  ( m = N -> ( F ` m ) = ( F ` N ) )
93 92 eleq2d 
 |-  ( m = N -> ( y e. ( F ` m ) <-> y e. ( F ` N ) ) )
94 91 93 bibi12d 
 |-  ( m = N -> ( ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> ( E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` N ) ) ) )
95 94 albidv 
 |-  ( m = N -> ( A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) <-> A. y ( E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` N ) ) ) )
96 95 imbi2d 
 |-  ( m = N -> ( ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc m /\ ( ( f ` (/) ) = y /\ ( f ` suc m ) = X ) /\ A. a e. suc m ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` m ) ) ) <-> ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` N ) ) ) ) )
97 eqeq2 
 |-  ( x = X -> ( ( f ` 1o ) = x <-> ( f ` 1o ) = X ) )
98 97 anbi2d 
 |-  ( x = X -> ( ( ( f ` (/) ) = y /\ ( f ` 1o ) = x ) <-> ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) )
99 98 anbi2d 
 |-  ( x = X -> ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = x ) ) <-> ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) ) )
100 99 exbidv 
 |-  ( x = X -> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = x ) ) <-> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) ) )
101 vex 
 |-  y e. _V
102 vex 
 |-  x e. _V
103 101 102 ifex 
 |-  if ( b = (/) , y , x ) e. _V
104 eqid 
 |-  ( b e. suc 1o |-> if ( b = (/) , y , x ) ) = ( b e. suc 1o |-> if ( b = (/) , y , x ) )
105 103 104 fnmpti 
 |-  ( b e. suc 1o |-> if ( b = (/) , y , x ) ) Fn suc 1o
106 equid 
 |-  y = y
107 equid 
 |-  x = x
108 106 107 pm3.2i 
 |-  ( y = y /\ x = x )
109 1oex 
 |-  1o e. _V
110 109 sucex 
 |-  suc 1o e. _V
111 110 mptex 
 |-  ( b e. suc 1o |-> if ( b = (/) , y , x ) ) e. _V
112 fneq1 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( f Fn suc 1o <-> ( b e. suc 1o |-> if ( b = (/) , y , x ) ) Fn suc 1o ) )
113 fveq1 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( f ` (/) ) = ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) ` (/) ) )
114 1on 
 |-  1o e. On
115 114 onordi 
 |-  Ord 1o
116 0elsuc 
 |-  ( Ord 1o -> (/) e. suc 1o )
117 iftrue 
 |-  ( b = (/) -> if ( b = (/) , y , x ) = y )
118 117 104 101 fvmpt 
 |-  ( (/) e. suc 1o -> ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) ` (/) ) = y )
119 115 116 118 mp2b 
 |-  ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) ` (/) ) = y
120 113 119 eqtrdi 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( f ` (/) ) = y )
121 120 eqeq1d 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( ( f ` (/) ) = y <-> y = y ) )
122 fveq1 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( f ` 1o ) = ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) ` 1o ) )
123 109 sucid 
 |-  1o e. suc 1o
124 eqeq1 
 |-  ( b = 1o -> ( b = (/) <-> 1o = (/) ) )
125 124 ifbid 
 |-  ( b = 1o -> if ( b = (/) , y , x ) = if ( 1o = (/) , y , x ) )
126 1n0 
 |-  1o =/= (/)
127 126 neii 
 |-  -. 1o = (/)
128 127 iffalsei 
 |-  if ( 1o = (/) , y , x ) = x
129 125 128 eqtrdi 
 |-  ( b = 1o -> if ( b = (/) , y , x ) = x )
130 129 104 102 fvmpt 
 |-  ( 1o e. suc 1o -> ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) ` 1o ) = x )
131 123 130 ax-mp 
 |-  ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) ` 1o ) = x
132 122 131 eqtrdi 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( f ` 1o ) = x )
133 132 eqeq1d 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( ( f ` 1o ) = x <-> x = x ) )
134 121 133 anbi12d 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( ( ( f ` (/) ) = y /\ ( f ` 1o ) = x ) <-> ( y = y /\ x = x ) ) )
135 112 134 anbi12d 
 |-  ( f = ( b e. suc 1o |-> if ( b = (/) , y , x ) ) -> ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = x ) ) <-> ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) Fn suc 1o /\ ( y = y /\ x = x ) ) ) )
136 111 135 spcev 
 |-  ( ( ( b e. suc 1o |-> if ( b = (/) , y , x ) ) Fn suc 1o /\ ( y = y /\ x = x ) ) -> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = x ) ) )
137 105 108 136 mp2an 
 |-  E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = x ) )
138 100 137 vtoclg 
 |-  ( X e. A -> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) )
139 138 adantl 
 |-  ( ( R Se A /\ X e. A ) -> E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) )
140 139 biantrurd 
 |-  ( ( R Se A /\ X e. A ) -> ( ( y e. A /\ y R X ) <-> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ ( y e. A /\ y R X ) ) ) )
141 101 elpred 
 |-  ( X e. A -> ( y e. Pred ( R , A , X ) <-> ( y e. A /\ y R X ) ) )
142 141 adantl 
 |-  ( ( R Se A /\ X e. A ) -> ( y e. Pred ( R , A , X ) <-> ( y e. A /\ y R X ) ) )
143 brres 
 |-  ( X e. A -> ( y ( R |` A ) X <-> ( y e. A /\ y R X ) ) )
144 143 adantl 
 |-  ( ( R Se A /\ X e. A ) -> ( y ( R |` A ) X <-> ( y e. A /\ y R X ) ) )
145 144 anbi2d 
 |-  ( ( R Se A /\ X e. A ) -> ( ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) <-> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ ( y e. A /\ y R X ) ) ) )
146 140 142 145 3bitr4rd 
 |-  ( ( R Se A /\ X e. A ) -> ( ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) <-> y e. Pred ( R , A , X ) ) )
147 df-3an 
 |-  ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) )
148 breq12 
 |-  ( ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) -> ( ( f ` (/) ) ( R |` A ) ( f ` 1o ) <-> y ( R |` A ) X ) )
149 148 adantl 
 |-  ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) -> ( ( f ` (/) ) ( R |` A ) ( f ` 1o ) <-> y ( R |` A ) X ) )
150 149 pm5.32i 
 |-  ( ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) )
151 147 150 bitri 
 |-  ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) )
152 151 exbii 
 |-  ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> E. f ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) )
153 19.41v 
 |-  ( E. f ( ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) <-> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) )
154 152 153 bitri 
 |-  ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) )
155 154 a1i 
 |-  ( ( R Se A /\ X e. A ) -> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) ) /\ y ( R |` A ) X ) ) )
156 1 fveq1i 
 |-  ( F ` (/) ) = ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) )
157 setlikespec 
 |-  ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
158 157 ancoms 
 |-  ( ( R Se A /\ X e. A ) -> Pred ( R , A , X ) e. _V )
159 rdg0g 
 |-  ( Pred ( R , A , X ) e. _V -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) = Pred ( R , A , X ) )
160 158 159 syl 
 |-  ( ( R Se A /\ X e. A ) -> ( rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) ) ` (/) ) = Pred ( R , A , X ) )
161 156 160 eqtrid 
 |-  ( ( R Se A /\ X e. A ) -> ( F ` (/) ) = Pred ( R , A , X ) )
162 161 eleq2d 
 |-  ( ( R Se A /\ X e. A ) -> ( y e. ( F ` (/) ) <-> y e. Pred ( R , A , X ) ) )
163 146 155 162 3bitr4d 
 |-  ( ( R Se A /\ X e. A ) -> ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> y e. ( F ` (/) ) ) )
164 163 alrimiv 
 |-  ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc 1o /\ ( ( f ` (/) ) = y /\ ( f ` 1o ) = X ) /\ ( f ` (/) ) ( R |` A ) ( f ` 1o ) ) <-> y e. ( F ` (/) ) ) )
165 eliun 
 |-  ( y e. U_ z e. ( F ` n ) Pred ( R , A , z ) <-> E. z e. ( F ` n ) y e. Pred ( R , A , z ) )
166 df-rex 
 |-  ( E. z e. ( F ` n ) y e. Pred ( R , A , z ) <-> E. z ( z e. ( F ` n ) /\ y e. Pred ( R , A , z ) ) )
167 165 166 bitri 
 |-  ( y e. U_ z e. ( F ` n ) Pred ( R , A , z ) <-> E. z ( z e. ( F ` n ) /\ y e. Pred ( R , A , z ) ) )
168 101 elpred 
 |-  ( z e. _V -> ( y e. Pred ( R , A , z ) <-> ( y e. A /\ y R z ) ) )
169 168 elv 
 |-  ( y e. Pred ( R , A , z ) <-> ( y e. A /\ y R z ) )
170 169 anbi2i 
 |-  ( ( z e. ( F ` n ) /\ y e. Pred ( R , A , z ) ) <-> ( z e. ( F ` n ) /\ ( y e. A /\ y R z ) ) )
171 anbi1 
 |-  ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) -> ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) <-> ( z e. ( F ` n ) /\ ( y e. A /\ y R z ) ) ) )
172 170 171 bitr4id 
 |-  ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) -> ( ( z e. ( F ` n ) /\ y e. Pred ( R , A , z ) ) <-> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
173 172 alexbii 
 |-  ( A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) -> ( E. z ( z e. ( F ` n ) /\ y e. Pred ( R , A , z ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
174 173 3ad2ant3 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) /\ A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> ( E. z ( z e. ( F ` n ) /\ y e. Pred ( R , A , z ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
175 167 174 bitrid 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) /\ A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> ( y e. U_ z e. ( F ` n ) Pred ( R , A , z ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
176 nnon 
 |-  ( n e. _om -> n e. On )
177 fvex 
 |-  ( F ` n ) e. _V
178 1 ttrclselem1 
 |-  ( n e. _om -> ( F ` n ) C_ A )
179 178 adantr 
 |-  ( ( n e. _om /\ R Se A ) -> ( F ` n ) C_ A )
180 dfse3 
 |-  ( R Se A <-> A. z e. A Pred ( R , A , z ) e. _V )
181 180 biimpi 
 |-  ( R Se A -> A. z e. A Pred ( R , A , z ) e. _V )
182 181 adantl 
 |-  ( ( n e. _om /\ R Se A ) -> A. z e. A Pred ( R , A , z ) e. _V )
183 ssralv 
 |-  ( ( F ` n ) C_ A -> ( A. z e. A Pred ( R , A , z ) e. _V -> A. z e. ( F ` n ) Pred ( R , A , z ) e. _V ) )
184 179 182 183 sylc 
 |-  ( ( n e. _om /\ R Se A ) -> A. z e. ( F ` n ) Pred ( R , A , z ) e. _V )
185 184 adantrr 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) ) -> A. z e. ( F ` n ) Pred ( R , A , z ) e. _V )
186 iunexg 
 |-  ( ( ( F ` n ) e. _V /\ A. z e. ( F ` n ) Pred ( R , A , z ) e. _V ) -> U_ z e. ( F ` n ) Pred ( R , A , z ) e. _V )
187 177 185 186 sylancr 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) ) -> U_ z e. ( F ` n ) Pred ( R , A , z ) e. _V )
188 nfcv 
 |-  F/_ b Pred ( R , A , X )
189 nfcv 
 |-  F/_ b n
190 nfmpt1 
 |-  F/_ b ( b e. _V |-> U_ w e. b Pred ( R , A , w ) )
191 190 188 nfrdg 
 |-  F/_ b rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) )
192 1 191 nfcxfr 
 |-  F/_ b F
193 192 189 nffv 
 |-  F/_ b ( F ` n )
194 nfcv 
 |-  F/_ b Pred ( R , A , z )
195 193 194 nfiun 
 |-  F/_ b U_ z e. ( F ` n ) Pred ( R , A , z )
196 predeq3 
 |-  ( w = z -> Pred ( R , A , w ) = Pred ( R , A , z ) )
197 196 cbviunv 
 |-  U_ w e. b Pred ( R , A , w ) = U_ z e. b Pred ( R , A , z )
198 iuneq1 
 |-  ( b = ( F ` n ) -> U_ z e. b Pred ( R , A , z ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
199 197 198 eqtrid 
 |-  ( b = ( F ` n ) -> U_ w e. b Pred ( R , A , w ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
200 188 189 195 1 199 rdgsucmptf 
 |-  ( ( n e. On /\ U_ z e. ( F ` n ) Pred ( R , A , z ) e. _V ) -> ( F ` suc n ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
201 176 187 200 syl2an2r 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) ) -> ( F ` suc n ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
202 201 3adant3 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) /\ A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> ( F ` suc n ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
203 202 eleq2d 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) /\ A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> ( y e. ( F ` suc n ) <-> y e. U_ z e. ( F ` n ) Pred ( R , A , z ) ) )
204 eqeq2 
 |-  ( x = X -> ( ( f ` suc suc n ) = x <-> ( f ` suc suc n ) = X ) )
205 204 anbi2d 
 |-  ( x = X -> ( ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) <-> ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) ) )
206 205 3anbi2d 
 |-  ( x = X -> ( ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
207 206 exbidv 
 |-  ( x = X -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
208 eqeq2 
 |-  ( x = X -> ( ( g ` suc n ) = x <-> ( g ` suc n ) = X ) )
209 208 anbi2d 
 |-  ( x = X -> ( ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) <-> ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) ) )
210 209 3anbi2d 
 |-  ( x = X -> ( ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
211 210 exbidv 
 |-  ( x = X -> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
212 211 anbi1d 
 |-  ( x = X -> ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) <-> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
213 212 exbidv 
 |-  ( x = X -> ( E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
214 207 213 bibi12d 
 |-  ( x = X -> ( ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) <-> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) ) )
215 214 imbi2d 
 |-  ( x = X -> ( ( n e. _om -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) ) <-> ( n e. _om -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) ) ) )
216 fvex 
 |-  ( f ` suc b ) e. _V
217 eqid 
 |-  ( b e. suc suc n |-> ( f ` suc b ) ) = ( b e. suc suc n |-> ( f ` suc b ) )
218 216 217 fnmpti 
 |-  ( b e. suc suc n |-> ( f ` suc b ) ) Fn suc suc n
219 218 a1i 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( b e. suc suc n |-> ( f ` suc b ) ) Fn suc suc n )
220 peano2 
 |-  ( n e. _om -> suc n e. _om )
221 220 adantr 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> suc n e. _om )
222 nnord 
 |-  ( suc n e. _om -> Ord suc n )
223 221 222 syl 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> Ord suc n )
224 0elsuc 
 |-  ( Ord suc n -> (/) e. suc suc n )
225 223 224 syl 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> (/) e. suc suc n )
226 suceq 
 |-  ( b = (/) -> suc b = suc (/) )
227 226 fveq2d 
 |-  ( b = (/) -> ( f ` suc b ) = ( f ` suc (/) ) )
228 fvex 
 |-  ( f ` suc (/) ) e. _V
229 227 217 228 fvmpt 
 |-  ( (/) e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) )
230 225 229 syl 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) )
231 vex 
 |-  n e. _V
232 231 sucex 
 |-  suc n e. _V
233 232 sucid 
 |-  suc n e. suc suc n
234 suceq 
 |-  ( b = suc n -> suc b = suc suc n )
235 234 fveq2d 
 |-  ( b = suc n -> ( f ` suc b ) = ( f ` suc suc n ) )
236 fvex 
 |-  ( f ` suc suc n ) e. _V
237 235 217 236 fvmpt 
 |-  ( suc n e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = ( f ` suc suc n ) )
238 233 237 mp1i 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = ( f ` suc suc n ) )
239 simpr2r 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( f ` suc suc n ) = x )
240 238 239 eqtrd 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = x )
241 fveq2 
 |-  ( a = suc c -> ( f ` a ) = ( f ` suc c ) )
242 suceq 
 |-  ( a = suc c -> suc a = suc suc c )
243 242 fveq2d 
 |-  ( a = suc c -> ( f ` suc a ) = ( f ` suc suc c ) )
244 241 243 breq12d 
 |-  ( a = suc c -> ( ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` suc c ) ( R |` A ) ( f ` suc suc c ) ) )
245 simplr3 
 |-  ( ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) /\ c e. suc n ) -> A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) )
246 ordsucelsuc 
 |-  ( Ord suc n -> ( c e. suc n <-> suc c e. suc suc n ) )
247 223 246 syl 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( c e. suc n <-> suc c e. suc suc n ) )
248 247 biimpa 
 |-  ( ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) /\ c e. suc n ) -> suc c e. suc suc n )
249 244 245 248 rspcdva 
 |-  ( ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) /\ c e. suc n ) -> ( f ` suc c ) ( R |` A ) ( f ` suc suc c ) )
250 elelsuc 
 |-  ( c e. suc n -> c e. suc suc n )
251 suceq 
 |-  ( b = c -> suc b = suc c )
252 251 fveq2d 
 |-  ( b = c -> ( f ` suc b ) = ( f ` suc c ) )
253 fvex 
 |-  ( f ` suc c ) e. _V
254 252 217 253 fvmpt 
 |-  ( c e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) = ( f ` suc c ) )
255 250 254 syl 
 |-  ( c e. suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) = ( f ` suc c ) )
256 255 adantl 
 |-  ( ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) /\ c e. suc n ) -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) = ( f ` suc c ) )
257 suceq 
 |-  ( b = suc c -> suc b = suc suc c )
258 257 fveq2d 
 |-  ( b = suc c -> ( f ` suc b ) = ( f ` suc suc c ) )
259 fvex 
 |-  ( f ` suc suc c ) e. _V
260 258 217 259 fvmpt 
 |-  ( suc c e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) = ( f ` suc suc c ) )
261 248 260 syl 
 |-  ( ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) /\ c e. suc n ) -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) = ( f ` suc suc c ) )
262 249 256 261 3brtr4d 
 |-  ( ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) /\ c e. suc n ) -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) ( R |` A ) ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) )
263 262 ralrimiva 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> A. c e. suc n ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) ( R |` A ) ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) )
264 232 sucex 
 |-  suc suc n e. _V
265 264 mptex 
 |-  ( b e. suc suc n |-> ( f ` suc b ) ) e. _V
266 fneq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g Fn suc suc n <-> ( b e. suc suc n |-> ( f ` suc b ) ) Fn suc suc n ) )
267 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` (/) ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) )
268 267 eqeq1d 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( ( g ` (/) ) = ( f ` suc (/) ) <-> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) ) )
269 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` suc n ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) )
270 269 eqeq1d 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( ( g ` suc n ) = x <-> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = x ) )
271 268 270 anbi12d 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) <-> ( ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) /\ ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = x ) ) )
272 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` c ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) )
273 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` suc c ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) )
274 272 273 breq12d 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( ( g ` c ) ( R |` A ) ( g ` suc c ) <-> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) ( R |` A ) ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) ) )
275 274 ralbidv 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) <-> A. c e. suc n ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) ( R |` A ) ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) ) )
276 266 271 275 3anbi123d 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( ( g Fn suc suc n /\ ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> ( ( b e. suc suc n |-> ( f ` suc b ) ) Fn suc suc n /\ ( ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) /\ ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = x ) /\ A. c e. suc n ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) ( R |` A ) ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) ) ) )
277 265 276 spcev 
 |-  ( ( ( b e. suc suc n |-> ( f ` suc b ) ) Fn suc suc n /\ ( ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) /\ ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = x ) /\ A. c e. suc n ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) ( R |` A ) ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) ) -> E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) )
278 219 230 240 263 277 syl121anc 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) )
279 simpr2l 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( f ` (/) ) = y )
280 15 fveq2d 
 |-  ( a = (/) -> ( f ` suc a ) = ( f ` suc (/) ) )
281 14 280 breq12d 
 |-  ( a = (/) -> ( ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` (/) ) ( R |` A ) ( f ` suc (/) ) ) )
282 simpr3 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) )
283 281 282 225 rspcdva 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> ( f ` (/) ) ( R |` A ) ( f ` suc (/) ) )
284 279 283 eqbrtrrd 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> y ( R |` A ) ( f ` suc (/) ) )
285 eqeq2 
 |-  ( z = ( f ` suc (/) ) -> ( ( g ` (/) ) = z <-> ( g ` (/) ) = ( f ` suc (/) ) ) )
286 285 anbi1d 
 |-  ( z = ( f ` suc (/) ) -> ( ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) <-> ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) ) )
287 286 3anbi2d 
 |-  ( z = ( f ` suc (/) ) -> ( ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> ( g Fn suc suc n /\ ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
288 287 exbidv 
 |-  ( z = ( f ` suc (/) ) -> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) ) )
289 breq2 
 |-  ( z = ( f ` suc (/) ) -> ( y ( R |` A ) z <-> y ( R |` A ) ( f ` suc (/) ) ) )
290 288 289 anbi12d 
 |-  ( z = ( f ` suc (/) ) -> ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) <-> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) ( f ` suc (/) ) ) ) )
291 228 290 spcev 
 |-  ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) ( f ` suc (/) ) ) -> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) )
292 278 284 291 syl2anc 
 |-  ( ( n e. _om /\ ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) -> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) )
293 292 ex 
 |-  ( n e. _om -> ( ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) -> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) ) )
294 293 exlimdv 
 |-  ( n e. _om -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) -> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) ) )
295 fvex 
 |-  ( g ` U. b ) e. _V
296 101 295 ifex 
 |-  if ( b = (/) , y , ( g ` U. b ) ) e. _V
297 eqid 
 |-  ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) )
298 296 297 fnmpti 
 |-  ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) Fn suc suc suc n
299 298 a1i 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) Fn suc suc suc n )
300 peano2 
 |-  ( suc n e. _om -> suc suc n e. _om )
301 220 300 syl 
 |-  ( n e. _om -> suc suc n e. _om )
302 301 3ad2ant1 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> suc suc n e. _om )
303 nnord 
 |-  ( suc suc n e. _om -> Ord suc suc n )
304 302 303 syl 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> Ord suc suc n )
305 0elsuc 
 |-  ( Ord suc suc n -> (/) e. suc suc suc n )
306 304 305 syl 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> (/) e. suc suc suc n )
307 iftrue 
 |-  ( b = (/) -> if ( b = (/) , y , ( g ` U. b ) ) = y )
308 307 297 101 fvmpt 
 |-  ( (/) e. suc suc suc n -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) = y )
309 306 308 syl 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) = y )
310 264 sucid 
 |-  suc suc n e. suc suc suc n
311 eqeq1 
 |-  ( b = suc suc n -> ( b = (/) <-> suc suc n = (/) ) )
312 unieq 
 |-  ( b = suc suc n -> U. b = U. suc suc n )
313 312 fveq2d 
 |-  ( b = suc suc n -> ( g ` U. b ) = ( g ` U. suc suc n ) )
314 311 313 ifbieq2d 
 |-  ( b = suc suc n -> if ( b = (/) , y , ( g ` U. b ) ) = if ( suc suc n = (/) , y , ( g ` U. suc suc n ) ) )
315 nsuceq0 
 |-  suc suc n =/= (/)
316 315 neii 
 |-  -. suc suc n = (/)
317 316 iffalsei 
 |-  if ( suc suc n = (/) , y , ( g ` U. suc suc n ) ) = ( g ` U. suc suc n )
318 314 317 eqtrdi 
 |-  ( b = suc suc n -> if ( b = (/) , y , ( g ` U. b ) ) = ( g ` U. suc suc n ) )
319 fvex 
 |-  ( g ` U. suc suc n ) e. _V
320 318 297 319 fvmpt 
 |-  ( suc suc n e. suc suc suc n -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) = ( g ` U. suc suc n ) )
321 310 320 mp1i 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) = ( g ` U. suc suc n ) )
322 220 3ad2ant1 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> suc n e. _om )
323 322 222 syl 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> Ord suc n )
324 ordunisuc 
 |-  ( Ord suc n -> U. suc suc n = suc n )
325 323 324 syl 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> U. suc suc n = suc n )
326 325 fveq2d 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( g ` U. suc suc n ) = ( g ` suc n ) )
327 simp22r 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( g ` suc n ) = x )
328 321 326 327 3eqtrd 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) = x )
329 simpl3 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a = (/) ) -> y ( R |` A ) z )
330 iftrue 
 |-  ( a = (/) -> if ( a = (/) , y , ( g ` U. a ) ) = y )
331 330 adantl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a = (/) ) -> if ( a = (/) , y , ( g ` U. a ) ) = y )
332 fveq2 
 |-  ( a = (/) -> ( g ` a ) = ( g ` (/) ) )
333 simp22l 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( g ` (/) ) = z )
334 332 333 sylan9eqr 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a = (/) ) -> ( g ` a ) = z )
335 329 331 334 3brtr4d 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a = (/) ) -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) )
336 335 ex 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( a = (/) -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) ) )
337 336 adantr 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( a = (/) -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) ) )
338 ordsucelsuc 
 |-  ( Ord suc n -> ( b e. suc n <-> suc b e. suc suc n ) )
339 323 338 syl 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( b e. suc n <-> suc b e. suc suc n ) )
340 elnn 
 |-  ( ( b e. suc n /\ suc n e. _om ) -> b e. _om )
341 322 340 sylan2 
 |-  ( ( b e. suc n /\ ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) ) -> b e. _om )
342 341 ancoms 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ b e. suc n ) -> b e. _om )
343 nnord 
 |-  ( b e. _om -> Ord b )
344 342 343 syl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ b e. suc n ) -> Ord b )
345 ordunisuc 
 |-  ( Ord b -> U. suc b = b )
346 344 345 syl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ b e. suc n ) -> U. suc b = b )
347 346 fveq2d 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ b e. suc n ) -> ( g ` U. suc b ) = ( g ` b ) )
348 simp23 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) )
349 fveq2 
 |-  ( c = b -> ( g ` c ) = ( g ` b ) )
350 suceq 
 |-  ( c = b -> suc c = suc b )
351 350 fveq2d 
 |-  ( c = b -> ( g ` suc c ) = ( g ` suc b ) )
352 349 351 breq12d 
 |-  ( c = b -> ( ( g ` c ) ( R |` A ) ( g ` suc c ) <-> ( g ` b ) ( R |` A ) ( g ` suc b ) ) )
353 352 rspcv 
 |-  ( b e. suc n -> ( A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) -> ( g ` b ) ( R |` A ) ( g ` suc b ) ) )
354 348 353 mpan9 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ b e. suc n ) -> ( g ` b ) ( R |` A ) ( g ` suc b ) )
355 347 354 eqbrtrd 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ b e. suc n ) -> ( g ` U. suc b ) ( R |` A ) ( g ` suc b ) )
356 355 ex 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( b e. suc n -> ( g ` U. suc b ) ( R |` A ) ( g ` suc b ) ) )
357 339 356 sylbird 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( suc b e. suc suc n -> ( g ` U. suc b ) ( R |` A ) ( g ` suc b ) ) )
358 357 imp 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ suc b e. suc suc n ) -> ( g ` U. suc b ) ( R |` A ) ( g ` suc b ) )
359 eleq1 
 |-  ( a = suc b -> ( a e. suc suc n <-> suc b e. suc suc n ) )
360 359 anbi2d 
 |-  ( a = suc b -> ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) <-> ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ suc b e. suc suc n ) ) )
361 eqeq1 
 |-  ( a = suc b -> ( a = (/) <-> suc b = (/) ) )
362 unieq 
 |-  ( a = suc b -> U. a = U. suc b )
363 362 fveq2d 
 |-  ( a = suc b -> ( g ` U. a ) = ( g ` U. suc b ) )
364 361 363 ifbieq2d 
 |-  ( a = suc b -> if ( a = (/) , y , ( g ` U. a ) ) = if ( suc b = (/) , y , ( g ` U. suc b ) ) )
365 nsuceq0 
 |-  suc b =/= (/)
366 365 neii 
 |-  -. suc b = (/)
367 366 iffalsei 
 |-  if ( suc b = (/) , y , ( g ` U. suc b ) ) = ( g ` U. suc b )
368 364 367 eqtrdi 
 |-  ( a = suc b -> if ( a = (/) , y , ( g ` U. a ) ) = ( g ` U. suc b ) )
369 fveq2 
 |-  ( a = suc b -> ( g ` a ) = ( g ` suc b ) )
370 368 369 breq12d 
 |-  ( a = suc b -> ( if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) <-> ( g ` U. suc b ) ( R |` A ) ( g ` suc b ) ) )
371 360 370 imbi12d 
 |-  ( a = suc b -> ( ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) ) <-> ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ suc b e. suc suc n ) -> ( g ` U. suc b ) ( R |` A ) ( g ` suc b ) ) ) )
372 358 371 mpbiri 
 |-  ( a = suc b -> ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) ) )
373 372 com12 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( a = suc b -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) ) )
374 373 rexlimdvw 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( E. b e. _om a = suc b -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) ) )
375 elnn 
 |-  ( ( a e. suc suc n /\ suc suc n e. _om ) -> a e. _om )
376 375 ancoms 
 |-  ( ( suc suc n e. _om /\ a e. suc suc n ) -> a e. _om )
377 302 376 sylan 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> a e. _om )
378 nn0suc 
 |-  ( a e. _om -> ( a = (/) \/ E. b e. _om a = suc b ) )
379 377 378 syl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( a = (/) \/ E. b e. _om a = suc b ) )
380 337 374 379 mpjaod 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) )
381 elelsuc 
 |-  ( a e. suc suc n -> a e. suc suc suc n )
382 eqeq1 
 |-  ( b = a -> ( b = (/) <-> a = (/) ) )
383 unieq 
 |-  ( b = a -> U. b = U. a )
384 383 fveq2d 
 |-  ( b = a -> ( g ` U. b ) = ( g ` U. a ) )
385 382 384 ifbieq2d 
 |-  ( b = a -> if ( b = (/) , y , ( g ` U. b ) ) = if ( a = (/) , y , ( g ` U. a ) ) )
386 fvex 
 |-  ( g ` U. a ) e. _V
387 101 386 ifex 
 |-  if ( a = (/) , y , ( g ` U. a ) ) e. _V
388 385 297 387 fvmpt 
 |-  ( a e. suc suc suc n -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) = if ( a = (/) , y , ( g ` U. a ) ) )
389 381 388 syl 
 |-  ( a e. suc suc n -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) = if ( a = (/) , y , ( g ` U. a ) ) )
390 389 adantl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) = if ( a = (/) , y , ( g ` U. a ) ) )
391 ordsucelsuc 
 |-  ( Ord suc suc n -> ( a e. suc suc n <-> suc a e. suc suc suc n ) )
392 304 391 syl 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> ( a e. suc suc n <-> suc a e. suc suc suc n ) )
393 392 biimpa 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> suc a e. suc suc suc n )
394 eqeq1 
 |-  ( b = suc a -> ( b = (/) <-> suc a = (/) ) )
395 unieq 
 |-  ( b = suc a -> U. b = U. suc a )
396 395 fveq2d 
 |-  ( b = suc a -> ( g ` U. b ) = ( g ` U. suc a ) )
397 394 396 ifbieq2d 
 |-  ( b = suc a -> if ( b = (/) , y , ( g ` U. b ) ) = if ( suc a = (/) , y , ( g ` U. suc a ) ) )
398 nsuceq0 
 |-  suc a =/= (/)
399 398 neii 
 |-  -. suc a = (/)
400 399 iffalsei 
 |-  if ( suc a = (/) , y , ( g ` U. suc a ) ) = ( g ` U. suc a )
401 397 400 eqtrdi 
 |-  ( b = suc a -> if ( b = (/) , y , ( g ` U. b ) ) = ( g ` U. suc a ) )
402 fvex 
 |-  ( g ` U. suc a ) e. _V
403 401 297 402 fvmpt 
 |-  ( suc a e. suc suc suc n -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) = ( g ` U. suc a ) )
404 393 403 syl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) = ( g ` U. suc a ) )
405 nnord 
 |-  ( a e. _om -> Ord a )
406 377 405 syl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> Ord a )
407 ordunisuc 
 |-  ( Ord a -> U. suc a = a )
408 406 407 syl 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> U. suc a = a )
409 408 fveq2d 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( g ` U. suc a ) = ( g ` a ) )
410 404 409 eqtrd 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) = ( g ` a ) )
411 380 390 410 3brtr4d 
 |-  ( ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) /\ a e. suc suc n ) -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) ( R |` A ) ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) )
412 411 ralrimiva 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> A. a e. suc suc n ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) ( R |` A ) ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) )
413 264 sucex 
 |-  suc suc suc n e. _V
414 413 mptex 
 |-  ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) e. _V
415 fneq1 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( f Fn suc suc suc n <-> ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) Fn suc suc suc n ) )
416 fveq1 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( f ` (/) ) = ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) )
417 416 eqeq1d 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( ( f ` (/) ) = y <-> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) = y ) )
418 fveq1 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( f ` suc suc n ) = ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) )
419 418 eqeq1d 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( ( f ` suc suc n ) = x <-> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) = x ) )
420 417 419 anbi12d 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) <-> ( ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) = y /\ ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) = x ) ) )
421 fveq1 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( f ` a ) = ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) )
422 fveq1 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( f ` suc a ) = ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) )
423 421 422 breq12d 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) ( R |` A ) ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) ) )
424 423 ralbidv 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) <-> A. a e. suc suc n ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) ( R |` A ) ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) ) )
425 415 420 424 3anbi123d 
 |-  ( f = ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) -> ( ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) Fn suc suc suc n /\ ( ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) = y /\ ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) = x ) /\ A. a e. suc suc n ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) ( R |` A ) ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) ) ) )
426 414 425 spcev 
 |-  ( ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) Fn suc suc suc n /\ ( ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) = y /\ ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc suc n ) = x ) /\ A. a e. suc suc n ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` a ) ( R |` A ) ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` suc a ) ) -> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) )
427 299 309 328 412 426 syl121anc 
 |-  ( ( n e. _om /\ ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) )
428 427 3exp 
 |-  ( n e. _om -> ( ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) -> ( y ( R |` A ) z -> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) ) )
429 428 exlimdv 
 |-  ( n e. _om -> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) -> ( y ( R |` A ) z -> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) ) )
430 429 impd 
 |-  ( n e. _om -> ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
431 430 exlimdv 
 |-  ( n e. _om -> ( E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) -> E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) ) )
432 294 431 impbid 
 |-  ( n e. _om -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) ) )
433 vex 
 |-  z e. _V
434 433 brresi 
 |-  ( y ( R |` A ) z <-> ( y e. A /\ y R z ) )
435 434 anbi2i 
 |-  ( ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) <-> ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) )
436 435 exbii 
 |-  ( E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ y ( R |` A ) z ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) )
437 432 436 bitrdi 
 |-  ( n e. _om -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
438 215 437 vtoclg 
 |-  ( X e. A -> ( n e. _om -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) ) )
439 438 impcom 
 |-  ( ( n e. _om /\ X e. A ) -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
440 439 adantrl 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) ) -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
441 440 3adant3 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) /\ A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> E. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) /\ ( y e. A /\ y R z ) ) ) )
442 175 203 441 3bitr4rd 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) /\ A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` suc n ) ) )
443 442 alrimiv 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) /\ A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> A. y ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` suc n ) ) )
444 443 3exp 
 |-  ( n e. _om -> ( ( R Se A /\ X e. A ) -> ( A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) -> A. y ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` suc n ) ) ) ) )
445 444 a2d 
 |-  ( n e. _om -> ( ( ( R Se A /\ X e. A ) -> A. z ( E. g ( g Fn suc suc n /\ ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) /\ A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) ) <-> z e. ( F ` n ) ) ) -> ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc suc n /\ ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) /\ A. a e. suc suc n ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` suc n ) ) ) ) )
446 27 68 82 96 164 445 finds 
 |-  ( N e. _om -> ( ( R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` N ) ) ) )
447 446 3impib 
 |-  ( ( N e. _om /\ R Se A /\ X e. A ) -> A. y ( E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` N ) ) )
448 447 19.21bi 
 |-  ( ( N e. _om /\ R Se A /\ X e. A ) -> ( E. f ( f Fn suc suc N /\ ( ( f ` (/) ) = y /\ ( f ` suc N ) = X ) /\ A. a e. suc N ( f ` a ) ( R |` A ) ( f ` suc a ) ) <-> y e. ( F ` N ) ) )