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 bilani 
 |-  ( ( n e. _om /\ R Se A ) -> A. z e. A Pred ( R , A , z ) e. _V )
182 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 ) )
183 179 181 182 sylc 
 |-  ( ( n e. _om /\ R Se A ) -> A. z e. ( F ` n ) Pred ( R , A , z ) e. _V )
184 183 adantrr 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) ) -> A. z e. ( F ` n ) Pred ( R , A , z ) e. _V )
185 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 )
186 177 184 185 sylancr 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) ) -> U_ z e. ( F ` n ) Pred ( R , A , z ) e. _V )
187 nfcv 
 |-  F/_ b Pred ( R , A , X )
188 nfcv 
 |-  F/_ b n
189 nfmpt1 
 |-  F/_ b ( b e. _V |-> U_ w e. b Pred ( R , A , w ) )
190 189 187 nfrdg 
 |-  F/_ b rec ( ( b e. _V |-> U_ w e. b Pred ( R , A , w ) ) , Pred ( R , A , X ) )
191 1 190 nfcxfr 
 |-  F/_ b F
192 191 188 nffv 
 |-  F/_ b ( F ` n )
193 nfcv 
 |-  F/_ b Pred ( R , A , z )
194 192 193 nfiun 
 |-  F/_ b U_ z e. ( F ` n ) Pred ( R , A , z )
195 predeq3 
 |-  ( w = z -> Pred ( R , A , w ) = Pred ( R , A , z ) )
196 195 cbviunv 
 |-  U_ w e. b Pred ( R , A , w ) = U_ z e. b Pred ( R , A , z )
197 iuneq1 
 |-  ( b = ( F ` n ) -> U_ z e. b Pred ( R , A , z ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
198 196 197 eqtrid 
 |-  ( b = ( F ` n ) -> U_ w e. b Pred ( R , A , w ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
199 187 188 194 1 198 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 ) )
200 176 186 199 syl2an2r 
 |-  ( ( n e. _om /\ ( R Se A /\ X e. A ) ) -> ( F ` suc n ) = U_ z e. ( F ` n ) Pred ( R , A , z ) )
201 200 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 ) )
202 201 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 ) ) )
203 eqeq2 
 |-  ( x = X -> ( ( f ` suc suc n ) = x <-> ( f ` suc suc n ) = X ) )
204 203 anbi2d 
 |-  ( x = X -> ( ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = x ) <-> ( ( f ` (/) ) = y /\ ( f ` suc suc n ) = X ) ) )
205 204 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 ) ) ) )
206 205 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 ) ) ) )
207 eqeq2 
 |-  ( x = X -> ( ( g ` suc n ) = x <-> ( g ` suc n ) = X ) )
208 207 anbi2d 
 |-  ( x = X -> ( ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) <-> ( ( g ` (/) ) = z /\ ( g ` suc n ) = X ) ) )
209 208 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 ) ) ) )
210 209 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 ) ) ) )
211 210 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 ) ) ) )
212 211 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 ) ) ) )
213 206 212 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 ) ) ) ) )
214 213 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 ) ) ) ) ) )
215 fvex 
 |-  ( f ` suc b ) e. _V
216 eqid 
 |-  ( b e. suc suc n |-> ( f ` suc b ) ) = ( b e. suc suc n |-> ( f ` suc b ) )
217 215 216 fnmpti 
 |-  ( b e. suc suc n |-> ( f ` suc b ) ) Fn suc suc n
218 217 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 )
219 peano2 
 |-  ( n e. _om -> suc n e. _om )
220 219 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 )
221 nnord 
 |-  ( suc n e. _om -> Ord suc n )
222 220 221 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 )
223 0elsuc 
 |-  ( Ord suc n -> (/) e. suc suc n )
224 222 223 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 )
225 suceq 
 |-  ( b = (/) -> suc b = suc (/) )
226 225 fveq2d 
 |-  ( b = (/) -> ( f ` suc b ) = ( f ` suc (/) ) )
227 fvex 
 |-  ( f ` suc (/) ) e. _V
228 226 216 227 fvmpt 
 |-  ( (/) e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) )
229 224 228 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 (/) ) )
230 vex 
 |-  n e. _V
231 230 sucex 
 |-  suc n e. _V
232 231 sucid 
 |-  suc n e. suc suc n
233 suceq 
 |-  ( b = suc n -> suc b = suc suc n )
234 233 fveq2d 
 |-  ( b = suc n -> ( f ` suc b ) = ( f ` suc suc n ) )
235 fvex 
 |-  ( f ` suc suc n ) e. _V
236 234 216 235 fvmpt 
 |-  ( suc n e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) = ( f ` suc suc n ) )
237 232 236 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 ) )
238 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 )
239 237 238 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 )
240 fveq2 
 |-  ( a = suc c -> ( f ` a ) = ( f ` suc c ) )
241 suceq 
 |-  ( a = suc c -> suc a = suc suc c )
242 241 fveq2d 
 |-  ( a = suc c -> ( f ` suc a ) = ( f ` suc suc c ) )
243 240 242 breq12d 
 |-  ( a = suc c -> ( ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` suc c ) ( R |` A ) ( f ` suc suc c ) ) )
244 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 ) )
245 ordsucelsuc 
 |-  ( Ord suc n -> ( c e. suc n <-> suc c e. suc suc n ) )
246 222 245 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 ) )
247 246 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 )
248 243 244 247 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 ) )
249 elelsuc 
 |-  ( c e. suc n -> c e. suc suc n )
250 suceq 
 |-  ( b = c -> suc b = suc c )
251 250 fveq2d 
 |-  ( b = c -> ( f ` suc b ) = ( f ` suc c ) )
252 fvex 
 |-  ( f ` suc c ) e. _V
253 251 216 252 fvmpt 
 |-  ( c e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) = ( f ` suc c ) )
254 249 253 syl 
 |-  ( c e. suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) = ( f ` suc c ) )
255 254 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 ) )
256 suceq 
 |-  ( b = suc c -> suc b = suc suc c )
257 256 fveq2d 
 |-  ( b = suc c -> ( f ` suc b ) = ( f ` suc suc c ) )
258 fvex 
 |-  ( f ` suc suc c ) e. _V
259 257 216 258 fvmpt 
 |-  ( suc c e. suc suc n -> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) = ( f ` suc suc c ) )
260 247 259 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 ) )
261 248 255 260 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 ) )
262 261 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 ) )
263 231 sucex 
 |-  suc suc n e. _V
264 263 mptex 
 |-  ( b e. suc suc n |-> ( f ` suc b ) ) e. _V
265 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 ) )
266 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` (/) ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) )
267 266 eqeq1d 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( ( g ` (/) ) = ( f ` suc (/) ) <-> ( ( b e. suc suc n |-> ( f ` suc b ) ) ` (/) ) = ( f ` suc (/) ) ) )
268 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` suc n ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc n ) )
269 268 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 ) )
270 267 269 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 ) ) )
271 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` c ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` c ) )
272 fveq1 
 |-  ( g = ( b e. suc suc n |-> ( f ` suc b ) ) -> ( g ` suc c ) = ( ( b e. suc suc n |-> ( f ` suc b ) ) ` suc c ) )
273 271 272 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 ) ) )
274 273 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 ) ) )
275 265 270 274 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 ) ) ) )
276 264 275 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 ) ) )
277 218 229 239 262 276 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 ) ) )
278 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 )
279 15 fveq2d 
 |-  ( a = (/) -> ( f ` suc a ) = ( f ` suc (/) ) )
280 14 279 breq12d 
 |-  ( a = (/) -> ( ( f ` a ) ( R |` A ) ( f ` suc a ) <-> ( f ` (/) ) ( R |` A ) ( f ` suc (/) ) ) )
281 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 ) )
282 280 281 224 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 (/) ) )
283 278 282 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 (/) ) )
284 eqeq2 
 |-  ( z = ( f ` suc (/) ) -> ( ( g ` (/) ) = z <-> ( g ` (/) ) = ( f ` suc (/) ) ) )
285 284 anbi1d 
 |-  ( z = ( f ` suc (/) ) -> ( ( ( g ` (/) ) = z /\ ( g ` suc n ) = x ) <-> ( ( g ` (/) ) = ( f ` suc (/) ) /\ ( g ` suc n ) = x ) ) )
286 285 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 ) ) ) )
287 286 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 ) ) ) )
288 breq2 
 |-  ( z = ( f ` suc (/) ) -> ( y ( R |` A ) z <-> y ( R |` A ) ( f ` suc (/) ) ) )
289 287 288 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 (/) ) ) ) )
290 227 289 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 ) )
291 277 283 290 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 ) )
292 291 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 ) ) )
293 292 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 ) ) )
294 fvex 
 |-  ( g ` U. b ) e. _V
295 101 294 ifex 
 |-  if ( b = (/) , y , ( g ` U. b ) ) e. _V
296 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 ) ) )
297 295 296 fnmpti 
 |-  ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) Fn suc suc suc n
298 297 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 )
299 peano2 
 |-  ( suc n e. _om -> suc suc n e. _om )
300 219 299 syl 
 |-  ( n e. _om -> suc suc n e. _om )
301 300 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 )
302 nnord 
 |-  ( suc suc n e. _om -> Ord suc suc n )
303 301 302 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 )
304 0elsuc 
 |-  ( Ord suc suc n -> (/) e. suc suc suc n )
305 303 304 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 )
306 iftrue 
 |-  ( b = (/) -> if ( b = (/) , y , ( g ` U. b ) ) = y )
307 306 296 101 fvmpt 
 |-  ( (/) e. suc suc suc n -> ( ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) ` (/) ) = y )
308 305 307 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 )
309 263 sucid 
 |-  suc suc n e. suc suc suc n
310 eqeq1 
 |-  ( b = suc suc n -> ( b = (/) <-> suc suc n = (/) ) )
311 unieq 
 |-  ( b = suc suc n -> U. b = U. suc suc n )
312 311 fveq2d 
 |-  ( b = suc suc n -> ( g ` U. b ) = ( g ` U. suc suc n ) )
313 310 312 ifbieq2d 
 |-  ( b = suc suc n -> if ( b = (/) , y , ( g ` U. b ) ) = if ( suc suc n = (/) , y , ( g ` U. suc suc n ) ) )
314 nsuceq0 
 |-  suc suc n =/= (/)
315 314 neii 
 |-  -. suc suc n = (/)
316 315 iffalsei 
 |-  if ( suc suc n = (/) , y , ( g ` U. suc suc n ) ) = ( g ` U. suc suc n )
317 313 316 eqtrdi 
 |-  ( b = suc suc n -> if ( b = (/) , y , ( g ` U. b ) ) = ( g ` U. suc suc n ) )
318 fvex 
 |-  ( g ` U. suc suc n ) e. _V
319 317 296 318 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 ) )
320 309 319 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 ) )
321 219 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 )
322 321 221 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 )
323 ordunisuc 
 |-  ( Ord suc n -> U. suc suc n = suc n )
324 322 323 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 )
325 324 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 ) )
326 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 )
327 320 325 326 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 )
328 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 )
329 iftrue 
 |-  ( a = (/) -> if ( a = (/) , y , ( g ` U. a ) ) = y )
330 329 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 )
331 fveq2 
 |-  ( a = (/) -> ( g ` a ) = ( g ` (/) ) )
332 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 )
333 331 332 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 )
334 328 330 333 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 ) )
335 334 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 ) ) )
336 335 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 ) ) )
337 ordsucelsuc 
 |-  ( Ord suc n -> ( b e. suc n <-> suc b e. suc suc n ) )
338 322 337 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 ) )
339 elnn 
 |-  ( ( b e. suc n /\ suc n e. _om ) -> b e. _om )
340 321 339 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 )
341 340 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 )
342 nnord 
 |-  ( b e. _om -> Ord b )
343 341 342 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 )
344 ordunisuc 
 |-  ( Ord b -> U. suc b = b )
345 343 344 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 )
346 345 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 ) )
347 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 ) )
348 fveq2 
 |-  ( c = b -> ( g ` c ) = ( g ` b ) )
349 suceq 
 |-  ( c = b -> suc c = suc b )
350 349 fveq2d 
 |-  ( c = b -> ( g ` suc c ) = ( g ` suc b ) )
351 348 350 breq12d 
 |-  ( c = b -> ( ( g ` c ) ( R |` A ) ( g ` suc c ) <-> ( g ` b ) ( R |` A ) ( g ` suc b ) ) )
352 351 rspcv 
 |-  ( b e. suc n -> ( A. c e. suc n ( g ` c ) ( R |` A ) ( g ` suc c ) -> ( g ` b ) ( R |` A ) ( g ` suc b ) ) )
353 347 352 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 ) )
354 346 353 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 ) )
355 354 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 ) ) )
356 338 355 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 ) ) )
357 356 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 ) )
358 eleq1 
 |-  ( a = suc b -> ( a e. suc suc n <-> suc b e. suc suc n ) )
359 358 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 ) ) )
360 eqeq1 
 |-  ( a = suc b -> ( a = (/) <-> suc b = (/) ) )
361 unieq 
 |-  ( a = suc b -> U. a = U. suc b )
362 361 fveq2d 
 |-  ( a = suc b -> ( g ` U. a ) = ( g ` U. suc b ) )
363 360 362 ifbieq2d 
 |-  ( a = suc b -> if ( a = (/) , y , ( g ` U. a ) ) = if ( suc b = (/) , y , ( g ` U. suc b ) ) )
364 nsuceq0 
 |-  suc b =/= (/)
365 364 neii 
 |-  -. suc b = (/)
366 365 iffalsei 
 |-  if ( suc b = (/) , y , ( g ` U. suc b ) ) = ( g ` U. suc b )
367 363 366 eqtrdi 
 |-  ( a = suc b -> if ( a = (/) , y , ( g ` U. a ) ) = ( g ` U. suc b ) )
368 fveq2 
 |-  ( a = suc b -> ( g ` a ) = ( g ` suc b ) )
369 367 368 breq12d 
 |-  ( a = suc b -> ( if ( a = (/) , y , ( g ` U. a ) ) ( R |` A ) ( g ` a ) <-> ( g ` U. suc b ) ( R |` A ) ( g ` suc b ) ) )
370 359 369 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 ) ) ) )
371 357 370 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 ) ) )
372 371 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 ) ) )
373 372 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 ) ) )
374 elnn 
 |-  ( ( a e. suc suc n /\ suc suc n e. _om ) -> a e. _om )
375 374 ancoms 
 |-  ( ( suc suc n e. _om /\ a e. suc suc n ) -> a e. _om )
376 301 375 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 )
377 nn0suc 
 |-  ( a e. _om -> ( a = (/) \/ E. b e. _om a = suc b ) )
378 376 377 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 ) )
379 336 373 378 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 ) )
380 elelsuc 
 |-  ( a e. suc suc n -> a e. suc suc suc n )
381 eqeq1 
 |-  ( b = a -> ( b = (/) <-> a = (/) ) )
382 unieq 
 |-  ( b = a -> U. b = U. a )
383 382 fveq2d 
 |-  ( b = a -> ( g ` U. b ) = ( g ` U. a ) )
384 381 383 ifbieq2d 
 |-  ( b = a -> if ( b = (/) , y , ( g ` U. b ) ) = if ( a = (/) , y , ( g ` U. a ) ) )
385 fvex 
 |-  ( g ` U. a ) e. _V
386 101 385 ifex 
 |-  if ( a = (/) , y , ( g ` U. a ) ) e. _V
387 384 296 386 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 ) ) )
388 380 387 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 ) ) )
389 388 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 ) ) )
390 ordsucelsuc 
 |-  ( Ord suc suc n -> ( a e. suc suc n <-> suc a e. suc suc suc n ) )
391 303 390 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 ) )
392 391 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 )
393 eqeq1 
 |-  ( b = suc a -> ( b = (/) <-> suc a = (/) ) )
394 unieq 
 |-  ( b = suc a -> U. b = U. suc a )
395 394 fveq2d 
 |-  ( b = suc a -> ( g ` U. b ) = ( g ` U. suc a ) )
396 393 395 ifbieq2d 
 |-  ( b = suc a -> if ( b = (/) , y , ( g ` U. b ) ) = if ( suc a = (/) , y , ( g ` U. suc a ) ) )
397 nsuceq0 
 |-  suc a =/= (/)
398 397 neii 
 |-  -. suc a = (/)
399 398 iffalsei 
 |-  if ( suc a = (/) , y , ( g ` U. suc a ) ) = ( g ` U. suc a )
400 396 399 eqtrdi 
 |-  ( b = suc a -> if ( b = (/) , y , ( g ` U. b ) ) = ( g ` U. suc a ) )
401 fvex 
 |-  ( g ` U. suc a ) e. _V
402 400 296 401 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 ) )
403 392 402 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 ) )
404 nnord 
 |-  ( a e. _om -> Ord a )
405 376 404 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 )
406 ordunisuc 
 |-  ( Ord a -> U. suc a = a )
407 405 406 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 )
408 407 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 ) )
409 403 408 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 ) )
410 379 389 409 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 ) )
411 410 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 ) )
412 263 sucex 
 |-  suc suc suc n e. _V
413 412 mptex 
 |-  ( b e. suc suc suc n |-> if ( b = (/) , y , ( g ` U. b ) ) ) e. _V
414 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 ) )
415 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 ) ) ) ` (/) ) )
416 415 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 ) )
417 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 ) )
418 417 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 ) )
419 416 418 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 ) ) )
420 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 ) )
421 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 ) )
422 420 421 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 ) ) )
423 422 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 ) ) )
424 414 419 423 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 ) ) ) )
425 413 424 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 ) ) )
426 298 308 327 411 425 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 ) ) )
427 426 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 ) ) ) ) )
428 427 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 ) ) ) ) )
429 428 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 ) ) ) )
430 429 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 ) ) ) )
431 293 430 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 ) ) )
432 vex 
 |-  z e. _V
433 432 brresi 
 |-  ( y ( R |` A ) z <-> ( y e. A /\ y R z ) )
434 433 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 ) ) )
435 434 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 ) ) )
436 431 435 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 ) ) ) )
437 214 436 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 ) ) ) ) )
438 437 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 ) ) ) )
439 438 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 ) ) ) )
440 439 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 ) ) ) )
441 175 202 440 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 ) ) )
442 441 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 ) ) )
443 442 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 ) ) ) ) )
444 443 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 ) ) ) ) )
445 27 68 82 96 164 444 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 ) ) ) )
446 445 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 ) ) )
447 446 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 ) ) )