Metamath Proof Explorer

Theorem fineqvnttrclse

Description: A counterexample demonstrating that ttrclse does not hold when all sets are finite. (Contributed by BTernaryTau, 12-Jan-2026)

Ref Expression
Hypotheses fineqvnttrclse.1 
|- R = { <. x , y >. | ( x e. A /\ x = suc y ) }
fineqvnttrclse.2 
|- A = _om
Assertion fineqvnttrclse 
|- ( Fin = _V -> ( R Se A /\ -. t++ ( R |` A ) Se A ) )

Proof

Step Hyp Ref Expression
1 fineqvnttrclse.1 
 |-  R = { <. x , y >. | ( x e. A /\ x = suc y ) }
2 fineqvnttrclse.2 
 |-  A = _om
3 ominf 
 |-  -. _om e. Fin
4 1onn 
 |-  1o e. _om
5 nnfi 
 |-  ( 1o e. _om -> 1o e. Fin )
6 4 5 ax-mp 
 |-  1o e. Fin
7 difinf 
 |-  ( ( -. _om e. Fin /\ 1o e. Fin ) -> -. ( _om \ 1o ) e. Fin )
8 3 6 7 mp2an 
 |-  -. ( _om \ 1o ) e. Fin
9 eleq2 
 |-  ( Fin = _V -> ( ( _om \ 1o ) e. Fin <-> ( _om \ 1o ) e. _V ) )
10 8 9 mtbii 
 |-  ( Fin = _V -> -. ( _om \ 1o ) e. _V )
11 difss 
 |-  ( _om \ 1o ) C_ _om
12 11 2 sseqtrri 
 |-  ( _om \ 1o ) C_ A
13 eldifi 
 |-  ( u e. ( _om \ 1o ) -> u e. _om )
14 eldifn 
 |-  ( u e. ( _om \ 1o ) -> -. u e. 1o )
15 0lt1o 
 |-  (/) e. 1o
16 eleq1 
 |-  ( u = (/) -> ( u e. 1o <-> (/) e. 1o ) )
17 15 16 mpbiri 
 |-  ( u = (/) -> u e. 1o )
18 17 necon3bi 
 |-  ( -. u e. 1o -> u =/= (/) )
19 14 18 syl 
 |-  ( u e. ( _om \ 1o ) -> u =/= (/) )
20 nnsuc 
 |-  ( ( u e. _om /\ u =/= (/) ) -> E. n e. _om u = suc n )
21 eqcom 
 |-  ( u = suc n <-> suc n = u )
22 21 rexbii 
 |-  ( E. n e. _om u = suc n <-> E. n e. _om suc n = u )
23 20 22 sylib 
 |-  ( ( u e. _om /\ u =/= (/) ) -> E. n e. _om suc n = u )
24 13 19 23 syl2anc 
 |-  ( u e. ( _om \ 1o ) -> E. n e. _om suc n = u )
25 sucexg 
 |-  ( n e. _V -> suc n e. _V )
26 25 elv 
 |-  suc n e. _V
27 26 sucex 
 |-  suc suc n e. _V
28 27 mptex 
 |-  ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) e. _V
29 28 a1i 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) e. _V )
30 fineqvnttrclselem1 
 |-  ( u e. ( _om \ 1o ) -> U. { d e. On | ( v +o d ) = u } e. _om )
31 30 elexd 
 |-  ( u e. ( _om \ 1o ) -> U. { d e. On | ( v +o d ) = u } e. _V )
32 31 ralrimivw 
 |-  ( u e. ( _om \ 1o ) -> A. v e. suc suc n U. { d e. On | ( v +o d ) = u } e. _V )
33 eqid 
 |-  ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } )
34 33 fnmpt 
 |-  ( A. v e. suc suc n U. { d e. On | ( v +o d ) = u } e. _V -> ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) Fn suc suc n )
35 32 34 syl 
 |-  ( u e. ( _om \ 1o ) -> ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) Fn suc suc n )
36 35 adantr 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) Fn suc suc n )
37 nnon 
 |-  ( u e. _om -> u e. On )
38 13 37 syl 
 |-  ( u e. ( _om \ 1o ) -> u e. On )
39 eloni 
 |-  ( u e. On -> Ord u )
40 38 39 syl 
 |-  ( u e. ( _om \ 1o ) -> Ord u )
41 40 adantr 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> Ord u )
42 ordeq 
 |-  ( suc n = u -> ( Ord suc n <-> Ord u ) )
43 42 adantl 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( Ord suc n <-> Ord u ) )
44 41 43 mpbird 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> Ord suc n )
45 0elsuc 
 |-  ( Ord suc n -> (/) e. suc suc n )
46 44 45 syl 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> (/) e. suc suc n )
47 simpl 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> u e. ( _om \ 1o ) )
48 oveq1 
 |-  ( v = (/) -> ( v +o d ) = ( (/) +o d ) )
49 48 eqeq1d 
 |-  ( v = (/) -> ( ( v +o d ) = u <-> ( (/) +o d ) = u ) )
50 49 rabbidv 
 |-  ( v = (/) -> { d e. On | ( v +o d ) = u } = { d e. On | ( (/) +o d ) = u } )
51 50 unieqd 
 |-  ( v = (/) -> U. { d e. On | ( v +o d ) = u } = U. { d e. On | ( (/) +o d ) = u } )
52 simpl 
 |-  ( ( (/) e. suc suc n /\ u e. ( _om \ 1o ) ) -> (/) e. suc suc n )
53 fineqvnttrclselem1 
 |-  ( u e. ( _om \ 1o ) -> U. { d e. On | ( (/) +o d ) = u } e. _om )
54 53 adantl 
 |-  ( ( (/) e. suc suc n /\ u e. ( _om \ 1o ) ) -> U. { d e. On | ( (/) +o d ) = u } e. _om )
55 33 51 52 54 fvmptd3 
 |-  ( ( (/) e. suc suc n /\ u e. ( _om \ 1o ) ) -> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = U. { d e. On | ( (/) +o d ) = u } )
56 oa0r 
 |-  ( d e. On -> ( (/) +o d ) = d )
57 56 eqeq1d 
 |-  ( d e. On -> ( ( (/) +o d ) = u <-> d = u ) )
58 57 rabbiia 
 |-  { d e. On | ( (/) +o d ) = u } = { d e. On | d = u }
59 rabsn 
 |-  ( u e. On -> { d e. On | d = u } = { u } )
60 58 59 eqtrid 
 |-  ( u e. On -> { d e. On | ( (/) +o d ) = u } = { u } )
61 60 unieqd 
 |-  ( u e. On -> U. { d e. On | ( (/) +o d ) = u } = U. { u } )
62 unisnv 
 |-  U. { u } = u
63 61 62 eqtrdi 
 |-  ( u e. On -> U. { d e. On | ( (/) +o d ) = u } = u )
64 38 63 syl 
 |-  ( u e. ( _om \ 1o ) -> U. { d e. On | ( (/) +o d ) = u } = u )
65 64 adantl 
 |-  ( ( (/) e. suc suc n /\ u e. ( _om \ 1o ) ) -> U. { d e. On | ( (/) +o d ) = u } = u )
66 55 65 eqtrd 
 |-  ( ( (/) e. suc suc n /\ u e. ( _om \ 1o ) ) -> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = u )
67 46 47 66 syl2anc 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = u )
68 oveq1 
 |-  ( v = suc n -> ( v +o d ) = ( suc n +o d ) )
69 68 eqeq1d 
 |-  ( v = suc n -> ( ( v +o d ) = u <-> ( suc n +o d ) = u ) )
70 69 rabbidv 
 |-  ( v = suc n -> { d e. On | ( v +o d ) = u } = { d e. On | ( suc n +o d ) = u } )
71 70 unieqd 
 |-  ( v = suc n -> U. { d e. On | ( v +o d ) = u } = U. { d e. On | ( suc n +o d ) = u } )
72 26 sucid 
 |-  suc n e. suc suc n
73 72 a1i 
 |-  ( u e. ( _om \ 1o ) -> suc n e. suc suc n )
74 fineqvnttrclselem1 
 |-  ( u e. ( _om \ 1o ) -> U. { d e. On | ( suc n +o d ) = u } e. _om )
75 33 71 73 74 fvmptd3 
 |-  ( u e. ( _om \ 1o ) -> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = U. { d e. On | ( suc n +o d ) = u } )
76 75 adantr 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = U. { d e. On | ( suc n +o d ) = u } )
77 oveq1 
 |-  ( suc n = u -> ( suc n +o d ) = ( u +o d ) )
78 77 eqeq1d 
 |-  ( suc n = u -> ( ( suc n +o d ) = u <-> ( u +o d ) = u ) )
79 78 ad2antlr 
 |-  ( ( ( u e. On /\ suc n = u ) /\ d e. On ) -> ( ( suc n +o d ) = u <-> ( u +o d ) = u ) )
80 oa0 
 |-  ( u e. On -> ( u +o (/) ) = u )
81 80 adantr 
 |-  ( ( u e. On /\ d e. On ) -> ( u +o (/) ) = u )
82 oveq2 
 |-  ( d = (/) -> ( u +o d ) = ( u +o (/) ) )
83 82 eqeq1d 
 |-  ( d = (/) -> ( ( u +o d ) = u <-> ( u +o (/) ) = u ) )
84 81 83 syl5ibrcom 
 |-  ( ( u e. On /\ d e. On ) -> ( d = (/) -> ( u +o d ) = u ) )
85 oveq2 
 |-  ( s = d -> ( u +o s ) = ( u +o d ) )
86 85 eqeq1d 
 |-  ( s = d -> ( ( u +o s ) = u <-> ( u +o d ) = u ) )
87 oveq2 
 |-  ( s = (/) -> ( u +o s ) = ( u +o (/) ) )
88 87 eqeq1d 
 |-  ( s = (/) -> ( ( u +o s ) = u <-> ( u +o (/) ) = u ) )
89 ssid 
 |-  u C_ u
90 oawordeu 
 |-  ( ( ( u e. On /\ u e. On ) /\ u C_ u ) -> E! s e. On ( u +o s ) = u )
91 89 90 mpan2 
 |-  ( ( u e. On /\ u e. On ) -> E! s e. On ( u +o s ) = u )
92 91 anidms 
 |-  ( u e. On -> E! s e. On ( u +o s ) = u )
93 92 3ad2ant1 
 |-  ( ( u e. On /\ d e. On /\ ( u +o d ) = u ) -> E! s e. On ( u +o s ) = u )
94 simp2 
 |-  ( ( u e. On /\ d e. On /\ ( u +o d ) = u ) -> d e. On )
95 0elon 
 |-  (/) e. On
96 95 a1i 
 |-  ( ( u e. On /\ d e. On /\ ( u +o d ) = u ) -> (/) e. On )
97 simp3 
 |-  ( ( u e. On /\ d e. On /\ ( u +o d ) = u ) -> ( u +o d ) = u )
98 80 3ad2ant1 
 |-  ( ( u e. On /\ d e. On /\ ( u +o d ) = u ) -> ( u +o (/) ) = u )
99 86 88 93 94 96 97 98 reu2eqd 
 |-  ( ( u e. On /\ d e. On /\ ( u +o d ) = u ) -> d = (/) )
100 99 3expia 
 |-  ( ( u e. On /\ d e. On ) -> ( ( u +o d ) = u -> d = (/) ) )
101 84 100 impbid 
 |-  ( ( u e. On /\ d e. On ) -> ( d = (/) <-> ( u +o d ) = u ) )
102 101 adantlr 
 |-  ( ( ( u e. On /\ suc n = u ) /\ d e. On ) -> ( d = (/) <-> ( u +o d ) = u ) )
103 79 102 bitr4d 
 |-  ( ( ( u e. On /\ suc n = u ) /\ d e. On ) -> ( ( suc n +o d ) = u <-> d = (/) ) )
104 103 rabbidva 
 |-  ( ( u e. On /\ suc n = u ) -> { d e. On | ( suc n +o d ) = u } = { d e. On | d = (/) } )
105 104 unieqd 
 |-  ( ( u e. On /\ suc n = u ) -> U. { d e. On | ( suc n +o d ) = u } = U. { d e. On | d = (/) } )
106 rabsn 
 |-  ( (/) e. On -> { d e. On | d = (/) } = { (/) } )
107 95 106 ax-mp 
 |-  { d e. On | d = (/) } = { (/) }
108 107 unieqi 
 |-  U. { d e. On | d = (/) } = U. { (/) }
109 0ex 
 |-  (/) e. _V
110 109 unisn 
 |-  U. { (/) } = (/)
111 108 110 eqtri 
 |-  U. { d e. On | d = (/) } = (/)
112 105 111 eqtrdi 
 |-  ( ( u e. On /\ suc n = u ) -> U. { d e. On | ( suc n +o d ) = u } = (/) )
113 38 112 sylan 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> U. { d e. On | ( suc n +o d ) = u } = (/) )
114 76 113 eqtrd 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = (/) )
115 67 114 jca 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = u /\ ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = (/) ) )
116 vex 
 |-  n e. _V
117 116 sucid 
 |-  n e. suc n
118 eleq2 
 |-  ( suc n = u -> ( n e. suc n <-> n e. u ) )
119 117 118 mpbii 
 |-  ( suc n = u -> n e. u )
120 oveq2 
 |-  ( d = e -> ( v +o d ) = ( v +o e ) )
121 120 eqeq1d 
 |-  ( d = e -> ( ( v +o d ) = u <-> ( v +o e ) = u ) )
122 121 cbvrabv 
 |-  { d e. On | ( v +o d ) = u } = { e e. On | ( v +o e ) = u }
123 122 unieqi 
 |-  U. { d e. On | ( v +o d ) = u } = U. { e e. On | ( v +o e ) = u }
124 123 mpteq2i 
 |-  ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) = ( v e. suc suc n |-> U. { e e. On | ( v +o e ) = u } )
125 1 2 124 fineqvnttrclselem3 
 |-  ( ( u e. ( _om \ 1o ) /\ n e. u ) -> A. a e. suc n ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` a ) R ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc a ) )
126 119 125 sylan2 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> A. a e. suc n ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` a ) R ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc a ) )
127 36 115 126 3jca 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) Fn suc suc n /\ ( ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = u /\ ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = (/) ) /\ A. a e. suc n ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` a ) R ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc a ) ) )
128 fneq1 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( f Fn suc suc n <-> ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) Fn suc suc n ) )
129 fveq1 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( f ` (/) ) = ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) )
130 129 eqeq1d 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( ( f ` (/) ) = u <-> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = u ) )
131 fveq1 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( f ` suc n ) = ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) )
132 131 eqeq1d 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( ( f ` suc n ) = (/) <-> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = (/) ) )
133 130 132 anbi12d 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( ( ( f ` (/) ) = u /\ ( f ` suc n ) = (/) ) <-> ( ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = u /\ ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = (/) ) ) )
134 fveq1 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( f ` a ) = ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` a ) )
135 fveq1 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( f ` suc a ) = ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc a ) )
136 134 135 breq12d 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( ( f ` a ) R ( f ` suc a ) <-> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` a ) R ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc a ) ) )
137 136 ralbidv 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( A. a e. suc n ( f ` a ) R ( f ` suc a ) <-> A. a e. suc n ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` a ) R ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc a ) ) )
138 128 133 137 3anbi123d 
 |-  ( f = ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) -> ( ( f Fn suc suc n /\ ( ( f ` (/) ) = u /\ ( f ` suc n ) = (/) ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) <-> ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) Fn suc suc n /\ ( ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` (/) ) = u /\ ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc n ) = (/) ) /\ A. a e. suc n ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` a ) R ( ( v e. suc suc n |-> U. { d e. On | ( v +o d ) = u } ) ` suc a ) ) ) )
139 29 127 138 spcedv 
 |-  ( ( u e. ( _om \ 1o ) /\ suc n = u ) -> E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = u /\ ( f ` suc n ) = (/) ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) )
140 139 ex 
 |-  ( u e. ( _om \ 1o ) -> ( suc n = u -> E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = u /\ ( f ` suc n ) = (/) ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) )
141 140 reximdv 
 |-  ( u e. ( _om \ 1o ) -> ( E. n e. _om suc n = u -> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = u /\ ( f ` suc n ) = (/) ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) )
142 24 141 mpd 
 |-  ( u e. ( _om \ 1o ) -> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = u /\ ( f ` suc n ) = (/) ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) )
143 brttrcl2 
 |-  ( u t++ R (/) <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = u /\ ( f ` suc n ) = (/) ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) )
144 142 143 sylibr 
 |-  ( u e. ( _om \ 1o ) -> u t++ R (/) )
145 1 relopabiv 
 |-  Rel R
146 1 dmeqi 
 |-  dom R = dom { <. x , y >. | ( x e. A /\ x = suc y ) }
147 dmopabss 
 |-  dom { <. x , y >. | ( x e. A /\ x = suc y ) } C_ A
148 146 147 eqsstri 
 |-  dom R C_ A
149 relssres 
 |-  ( ( Rel R /\ dom R C_ A ) -> ( R |` A ) = R )
150 145 148 149 mp2an 
 |-  ( R |` A ) = R
151 ttrcleq 
 |-  ( ( R |` A ) = R -> t++ ( R |` A ) = t++ R )
152 150 151 ax-mp 
 |-  t++ ( R |` A ) = t++ R
153 152 breqi 
 |-  ( u t++ ( R |` A ) (/) <-> u t++ R (/) )
154 144 153 sylibr 
 |-  ( u e. ( _om \ 1o ) -> u t++ ( R |` A ) (/) )
155 154 rgen 
 |-  A. u e. ( _om \ 1o ) u t++ ( R |` A ) (/)
156 ssrab 
 |-  ( ( _om \ 1o ) C_ { u e. A | u t++ ( R |` A ) (/) } <-> ( ( _om \ 1o ) C_ A /\ A. u e. ( _om \ 1o ) u t++ ( R |` A ) (/) ) )
157 12 155 156 mpbir2an 
 |-  ( _om \ 1o ) C_ { u e. A | u t++ ( R |` A ) (/) }
158 ssexg 
 |-  ( ( ( _om \ 1o ) C_ { u e. A | u t++ ( R |` A ) (/) } /\ { u e. A | u t++ ( R |` A ) (/) } e. _V ) -> ( _om \ 1o ) e. _V )
159 157 158 mpan 
 |-  ( { u e. A | u t++ ( R |` A ) (/) } e. _V -> ( _om \ 1o ) e. _V )
160 159 con3i 
 |-  ( -. ( _om \ 1o ) e. _V -> -. { u e. A | u t++ ( R |` A ) (/) } e. _V )
161 peano1 
 |-  (/) e. _om
162 161 2 eleqtrri 
 |-  (/) e. A
163 breq2 
 |-  ( t = (/) -> ( u t++ ( R |` A ) t <-> u t++ ( R |` A ) (/) ) )
164 163 rabbidv 
 |-  ( t = (/) -> { u e. A | u t++ ( R |` A ) t } = { u e. A | u t++ ( R |` A ) (/) } )
165 164 eleq1d 
 |-  ( t = (/) -> ( { u e. A | u t++ ( R |` A ) t } e. _V <-> { u e. A | u t++ ( R |` A ) (/) } e. _V ) )
166 165 rspcv 
 |-  ( (/) e. A -> ( A. t e. A { u e. A | u t++ ( R |` A ) t } e. _V -> { u e. A | u t++ ( R |` A ) (/) } e. _V ) )
167 162 166 ax-mp 
 |-  ( A. t e. A { u e. A | u t++ ( R |` A ) t } e. _V -> { u e. A | u t++ ( R |` A ) (/) } e. _V )
168 167 con3i 
 |-  ( -. { u e. A | u t++ ( R |` A ) (/) } e. _V -> -. A. t e. A { u e. A | u t++ ( R |` A ) t } e. _V )
169 10 160 168 3syl 
 |-  ( Fin = _V -> -. A. t e. A { u e. A | u t++ ( R |` A ) t } e. _V )
170 df-se 
 |-  ( t++ ( R |` A ) Se A <-> A. t e. A { u e. A | u t++ ( R |` A ) t } e. _V )
171 169 170 sylnibr 
 |-  ( Fin = _V -> -. t++ ( R |` A ) Se A )
172 vex 
 |-  w e. _V
173 vex 
 |-  z e. _V
174 eleq1w 
 |-  ( x = w -> ( x e. A <-> w e. A ) )
175 eqeq1 
 |-  ( x = w -> ( x = suc y <-> w = suc y ) )
176 174 175 anbi12d 
 |-  ( x = w -> ( ( x e. A /\ x = suc y ) <-> ( w e. A /\ w = suc y ) ) )
177 suceq 
 |-  ( y = z -> suc y = suc z )
178 177 eqeq2d 
 |-  ( y = z -> ( w = suc y <-> w = suc z ) )
179 178 anbi2d 
 |-  ( y = z -> ( ( w e. A /\ w = suc y ) <-> ( w e. A /\ w = suc z ) ) )
180 172 173 176 179 1 brab 
 |-  ( w R z <-> ( w e. A /\ w = suc z ) )
181 180 biimpi 
 |-  ( w R z -> ( w e. A /\ w = suc z ) )
182 181 adantl 
 |-  ( ( w e. A /\ w R z ) -> ( w e. A /\ w = suc z ) )
183 simpl 
 |-  ( ( w e. A /\ w = suc z ) -> w e. A )
184 180 biimpri 
 |-  ( ( w e. A /\ w = suc z ) -> w R z )
185 183 184 jca 
 |-  ( ( w e. A /\ w = suc z ) -> ( w e. A /\ w R z ) )
186 182 185 impbii 
 |-  ( ( w e. A /\ w R z ) <-> ( w e. A /\ w = suc z ) )
187 186 rabbia2 
 |-  { w e. A | w R z } = { w e. A | w = suc z }
188 173 sucex 
 |-  suc z e. _V
189 188 eueqi 
 |-  E! w w = suc z
190 euabex 
 |-  ( E! w w = suc z -> { w | w = suc z } e. _V )
191 189 190 ax-mp 
 |-  { w | w = suc z } e. _V
192 rabssab 
 |-  { w e. A | w = suc z } C_ { w | w = suc z }
193 191 192 ssexi 
 |-  { w e. A | w = suc z } e. _V
194 187 193 eqeltri 
 |-  { w e. A | w R z } e. _V
195 194 rgenw 
 |-  A. z e. A { w e. A | w R z } e. _V
196 df-se 
 |-  ( R Se A <-> A. z e. A { w e. A | w R z } e. _V )
197 195 196 mpbir 
 |-  R Se A
198 171 197 jctil 
 |-  ( Fin = _V -> ( R Se A /\ -. t++ ( R |` A ) Se A ) )