Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tartarmap Unicode version

Theorem tartarmap 25300
Description: The sequence  tar has its values in a Tarski's class. (Contributed by FL, 20-Mar-2011.)
Assertion
Ref Expression
tartarmap  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  B  e.  Y )  -> 
( ( tar `  <. X ,  Y >. ) `  B )  C_  ( tarskiMap `  X ) )

Proof of Theorem tartarmap
Dummy variables  x  w  z  b  c 
v  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 onelon 4417 . . 3  |-  ( ( Y  e.  On  /\  suc  B  e.  Y )  ->  suc  B  e.  On )
213adant1 973 . 2  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  B  e.  Y )  ->  suc  B  e.  On )
3 sucelon 4608 . . 3  |-  ( B  e.  On  <->  suc  B  e.  On )
4 suceq 4457 . . . . . . 7  |-  ( b  =  (/)  ->  suc  b  =  suc  (/) )
54eleq1d 2349 . . . . . 6  |-  ( b  =  (/)  ->  ( suc  b  e.  Y  <->  suc  (/)  e.  Y
) )
653anbi3d 1258 . . . . 5  |-  ( b  =  (/)  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  <->  ( X  e.  A  /\  Y  e.  On  /\  suc  (/) 
e.  Y ) ) )
7 fveq2 5525 . . . . . 6  |-  ( b  =  (/)  ->  ( ( tar `  <. X ,  Y >. ) `  b
)  =  ( ( tar `  <. X ,  Y >. ) `  (/) ) )
87sseq1d 3205 . . . . 5  |-  ( b  =  (/)  ->  ( ( ( tar `  <. X ,  Y >. ) `  b )  C_  ( tarskiMap `  X )  <->  ( ( tar `  <. X ,  Y >. ) `  (/) )  C_  (
tarskiMap `
 X ) ) )
96, 8imbi12d 311 . . . 4  |-  ( b  =  (/)  ->  ( ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  b ) 
C_  ( tarskiMap `  X
) )  <->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  (/) 
e.  Y )  -> 
( ( tar `  <. X ,  Y >. ) `  (/) )  C_  ( tarskiMap `  X ) ) ) )
10 suceq 4457 . . . . . . 7  |-  ( b  =  c  ->  suc  b  =  suc  c )
1110eleq1d 2349 . . . . . 6  |-  ( b  =  c  ->  ( suc  b  e.  Y  <->  suc  c  e.  Y ) )
12113anbi3d 1258 . . . . 5  |-  ( b  =  c  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  <->  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) ) )
13 fveq2 5525 . . . . . 6  |-  ( b  =  c  ->  (
( tar `  <. X ,  Y >. ) `  b )  =  ( ( tar `  <. X ,  Y >. ) `  c ) )
1413sseq1d 3205 . . . . 5  |-  ( b  =  c  ->  (
( ( tar `  <. X ,  Y >. ) `  b )  C_  ( tarskiMap `  X )  <->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) ) )
1512, 14imbi12d 311 . . . 4  |-  ( b  =  c  ->  (
( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  b )  C_  ( tarskiMap `  X ) )  <->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) ) ) )
16 suceq 4457 . . . . . . 7  |-  ( b  =  suc  c  ->  suc  b  =  suc  suc  c )
1716eleq1d 2349 . . . . . 6  |-  ( b  =  suc  c  -> 
( suc  b  e.  Y 
<->  suc  suc  c  e.  Y ) )
18173anbi3d 1258 . . . . 5  |-  ( b  =  suc  c  -> 
( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  <->  ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )
) )
19 fveq2 5525 . . . . . 6  |-  ( b  =  suc  c  -> 
( ( tar `  <. X ,  Y >. ) `  b )  =  ( ( tar `  <. X ,  Y >. ) `  suc  c ) )
2019sseq1d 3205 . . . . 5  |-  ( b  =  suc  c  -> 
( ( ( tar `  <. X ,  Y >. ) `  b ) 
C_  ( tarskiMap `  X
)  <->  ( ( tar `  <. X ,  Y >. ) `  suc  c
)  C_  ( tarskiMap `  X
) ) )
2118, 20imbi12d 311 . . . 4  |-  ( b  =  suc  c  -> 
( ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  b )  C_  ( tarskiMap `  X ) )  <->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  ( ( tar `  <. X ,  Y >. ) `  suc  c
)  C_  ( tarskiMap `  X
) ) ) )
22 suceq 4457 . . . . . . 7  |-  ( b  =  B  ->  suc  b  =  suc  B )
2322eleq1d 2349 . . . . . 6  |-  ( b  =  B  ->  ( suc  b  e.  Y  <->  suc 
B  e.  Y ) )
24233anbi3d 1258 . . . . 5  |-  ( b  =  B  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  <->  ( X  e.  A  /\  Y  e.  On  /\  suc  B  e.  Y ) ) )
25 fveq2 5525 . . . . . 6  |-  ( b  =  B  ->  (
( tar `  <. X ,  Y >. ) `  b )  =  ( ( tar `  <. X ,  Y >. ) `  B ) )
2625sseq1d 3205 . . . . 5  |-  ( b  =  B  ->  (
( ( tar `  <. X ,  Y >. ) `  b )  C_  ( tarskiMap `  X )  <->  ( ( tar `  <. X ,  Y >. ) `  B ) 
C_  ( tarskiMap `  X
) ) )
2724, 26imbi12d 311 . . . 4  |-  ( b  =  B  ->  (
( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  b )  C_  ( tarskiMap `  X ) )  <->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  B  e.  Y )  -> 
( ( tar `  <. X ,  Y >. ) `  B )  C_  ( tarskiMap `  X ) ) ) )
28 ne0i 3461 . . . . . 6  |-  ( suc  (/)  e.  Y  ->  Y  =/=  (/) )
29 vtare 25297 . . . . . 6  |-  ( ( X  e.  A  /\  Y  e.  On  /\  Y  =/=  (/) )  ->  (
( tar `  <. X ,  Y >. ) `  (/) )  =  { X } )
3028, 29syl3an3 1217 . . . . 5  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  (/) 
e.  Y )  -> 
( ( tar `  <. X ,  Y >. ) `  (/) )  =  { X } )
31 tskmid 8462 . . . . . . 7  |-  ( X  e.  A  ->  X  e.  ( tarskiMap `  X )
)
32313ad2ant1 976 . . . . . 6  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  (/) 
e.  Y )  ->  X  e.  ( tarskiMap `  X
) )
3332snssd 3760 . . . . 5  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  (/) 
e.  Y )  ->  { X }  C_  ( tarskiMap `  X ) )
3430, 33eqsstrd 3212 . . . 4  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  (/) 
e.  Y )  -> 
( ( tar `  <. X ,  Y >. ) `  (/) )  C_  ( tarskiMap `  X ) )
35 inss2 3390 . . . . . 6  |-  ( ( { v  |  E. y  e.  ( ( tar `  <. X ,  Y >. ) `  c ) ( v  C_  y  \/  v  =  ~P y ) }  u.  ~P ( ( tar `  <. X ,  Y >. ) `  c ) )  i^i  ( tarskiMap `  X )
)  C_  ( tarskiMap `  X
)
36 simp1 955 . . . . . . . . 9  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  X  e.  A
)
37 simp2 956 . . . . . . . . 9  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  Y  e.  On )
38 eloni 4402 . . . . . . . . . . . 12  |-  ( Y  e.  On  ->  Ord  Y )
39 ordtr 4406 . . . . . . . . . . . 12  |-  ( Ord 
Y  ->  Tr  Y
)
4038, 39syl 15 . . . . . . . . . . 11  |-  ( Y  e.  On  ->  Tr  Y )
41403ad2ant2 977 . . . . . . . . . 10  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  Tr  Y )
42 simp3 957 . . . . . . . . . 10  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  suc  suc  c  e.  Y )
43 trsuc 4476 . . . . . . . . . 10  |-  ( ( Tr  Y  /\  suc  suc  c  e.  Y )  ->  suc  c  e.  Y )
4441, 42, 43syl2anc 642 . . . . . . . . 9  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  suc  c  e.  Y )
4536, 37, 443jca 1132 . . . . . . . 8  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) )
46453ad2ant3 978 . . . . . . 7  |-  ( ( c  e.  On  /\  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  suc  c  e.  Y
) )  ->  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
)
47 vtarsu 25298 . . . . . . . 8  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( ( tar `  <. X ,  Y >. ) `  suc  c )  =  ( ( { v  |  E. y  e.  ( ( tar `  <. X ,  Y >. ) `  c ) ( v 
C_  y  \/  v  =  ~P y ) }  u.  ~P ( ( tar `  <. X ,  Y >. ) `  c
) )  i^i  ( tarskiMap `  X ) ) )
4847sseq1d 3205 . . . . . . 7  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( ( ( tar `  <. X ,  Y >. ) `  suc  c
)  C_  ( tarskiMap `  X
)  <->  ( ( { v  |  E. y  e.  ( ( tar `  <. X ,  Y >. ) `  c ) ( v 
C_  y  \/  v  =  ~P y ) }  u.  ~P ( ( tar `  <. X ,  Y >. ) `  c
) )  i^i  ( tarskiMap `  X ) )  C_  (
tarskiMap `
 X ) ) )
4946, 48syl 15 . . . . . 6  |-  ( ( c  e.  On  /\  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  suc  c  e.  Y
) )  ->  (
( ( tar `  <. X ,  Y >. ) `  suc  c )  C_  (
tarskiMap `
 X )  <->  ( ( { v  |  E. y  e.  ( ( tar `  <. X ,  Y >. ) `  c ) ( v  C_  y  \/  v  =  ~P y ) }  u.  ~P ( ( tar `  <. X ,  Y >. ) `  c ) )  i^i  ( tarskiMap `  X )
)  C_  ( tarskiMap `  X
) ) )
5035, 49mpbiri 224 . . . . 5  |-  ( ( c  e.  On  /\  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  suc  c  e.  Y
) )  ->  (
( tar `  <. X ,  Y >. ) `  suc  c )  C_  (
tarskiMap `
 X ) )
51503exp 1150 . . . 4  |-  ( c  e.  On  ->  (
( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  -> 
( ( X  e.  A  /\  Y  e.  On  /\  suc  suc  c  e.  Y )  ->  ( ( tar `  <. X ,  Y >. ) `  suc  c )  C_  (
tarskiMap `
 X ) ) ) )
52 simp31 991 . . . . . . 7  |-  ( ( Lim  b  /\  A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  X  e.  A )
53 simp32 992 . . . . . . 7  |-  ( ( Lim  b  /\  A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  Y  e.  On )
54 ordsuccl2 24515 . . . . . . . . . . 11  |-  ( ( Y  e.  On  /\  suc  b  e.  Y
)  ->  b  e.  Y )
55543adant1 973 . . . . . . . . . 10  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  b  e.  Y )
5655adantl 452 . . . . . . . . 9  |-  ( ( Lim  b  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  b  e.  Y )
57 simpl 443 . . . . . . . . 9  |-  ( ( Lim  b  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  Lim  b )
5856, 57jca 518 . . . . . . . 8  |-  ( ( Lim  b  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  ( b  e.  Y  /\  Lim  b
) )
59583adant2 974 . . . . . . 7  |-  ( ( Lim  b  /\  A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  ( b  e.  Y  /\  Lim  b
) )
60 vtarl 25299 . . . . . . 7  |-  ( ( X  e.  A  /\  Y  e.  On  /\  (
b  e.  Y  /\  Lim  b ) )  -> 
( ( tar `  <. X ,  Y >. ) `  b )  =  U. ( ( tar `  <. X ,  Y >. ) " b ) )
6152, 53, 59, 60syl3anc 1182 . . . . . 6  |-  ( ( Lim  b  /\  A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  ( ( tar `  <. X ,  Y >. ) `  b )  =  U. ( ( tar `  <. X ,  Y >. ) " b
) )
62 r19.27av 2681 . . . . . . . . . . 11  |-  ( ( A. c  e.  b  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
) )  ->  A. c  e.  b  ( (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
) )
63 ordon 4574 . . . . . . . . . . . . . . . . . . . . . 22  |-  Ord  On
64 ordtr1 4435 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Ord 
On  ->  ( ( suc  b  e.  Y  /\  Y  e.  On )  ->  suc  b  e.  On ) )
6563, 64ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( suc  b  e.  Y  /\  Y  e.  On )  ->  suc  b  e.  On )
66 sucelon 4608 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  e.  On  <->  suc  b  e.  On )
67 eloni 4402 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  e.  On  ->  Ord  b )
6866, 67sylbir 204 . . . . . . . . . . . . . . . . . . . . 21  |-  ( suc  b  e.  On  ->  Ord  b )
6965, 68syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( suc  b  e.  Y  /\  Y  e.  On )  ->  Ord  b )
7069ancoms 439 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Y  e.  On  /\  suc  b  e.  Y
)  ->  Ord  b )
71703adant1 973 . . . . . . . . . . . . . . . . . 18  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  Ord  b )
72 ordsucelsuc 4613 . . . . . . . . . . . . . . . . . . 19  |-  ( Ord  b  ->  ( c  e.  b  <->  suc  c  e.  suc  b ) )
73 simpl1 958 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  /\  suc  c  e. 
suc  b )  ->  X  e.  A )
74 simpl2 959 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  /\  suc  c  e. 
suc  b )  ->  Y  e.  On )
7538a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( X  e.  A  ->  ( Y  e.  On  ->  Ord 
Y ) )
76 ordtr1 4435 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( Ord 
Y  ->  ( ( suc  c  e.  suc  b  /\  suc  b  e.  Y )  ->  suc  c  e.  Y )
)
7776exp3acom23 1362 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Ord 
Y  ->  ( suc  b  e.  Y  ->  ( suc  c  e.  suc  b  ->  suc  c  e.  Y ) ) )
7875, 77syl6 29 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( X  e.  A  ->  ( Y  e.  On  ->  ( suc  b  e.  Y  ->  ( suc  c  e. 
suc  b  ->  suc  c  e.  Y )
) ) )
79783imp1 1164 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  /\  suc  c  e. 
suc  b )  ->  suc  c  e.  Y
)
8073, 74, 793jca 1132 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  /\  suc  c  e. 
suc  b )  -> 
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
) )
8180expcom 424 . . . . . . . . . . . . . . . . . . 19  |-  ( suc  c  e.  suc  b  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
) )
8272, 81syl6bi 219 . . . . . . . . . . . . . . . . . 18  |-  ( Ord  b  ->  ( c  e.  b  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
) ) ) )
8371, 82syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( c  e.  b  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
) ) )
8483pm2.43a 45 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( c  e.  b  ->  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) ) )
85 pm5.31 571 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  /\  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) ) )  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
) ) )
8685ex 423 . . . . . . . . . . . . . . . . 17  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  -> 
( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
) ) ) )
8786pm2.43a 45 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  -> 
( ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
)  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) ) ) )
8884, 87syl6 29 . . . . . . . . . . . . . . 15  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( c  e.  b  ->  ( ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  -> 
( ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
)  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) ) ) ) )
8988com3r 73 . . . . . . . . . . . . . 14  |-  ( ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  ->  ( c  e.  b  ->  ( ( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
) ) ) )
9089imp 418 . . . . . . . . . . . . 13  |-  ( ( ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
) )  ->  (
c  e.  b  -> 
( ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
)  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) ) ) )
9190impcom 419 . . . . . . . . . . . 12  |-  ( ( c  e.  b  /\  ( ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
) ) )  -> 
( ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
)  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) ) )
9291ralimiaa 2617 . . . . . . . . . . 11  |-  ( A. c  e.  b  (
( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
) )  ->  A. c  e.  b  ( (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
) )
93 r19.26 2675 . . . . . . . . . . . 12  |-  ( A. c  e.  b  (
( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
)  <->  ( A. c  e.  b  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
)  /\  A. c  e.  b  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y ) ) )
94 3simpa 952 . . . . . . . . . . . . . . 15  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( X  e.  A  /\  Y  e.  On ) )
9594ralimi 2618 . . . . . . . . . . . . . 14  |-  ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  A. c  e.  b  ( X  e.  A  /\  Y  e.  On ) )
96 valtar 25295 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( X  e.  A  /\  Y  e.  On )  ->  ( tar `  <. X ,  Y >. )  =  ( rec (
( x  e.  _V  |->  ( ( { w  |  E. z  e.  x  ( w  C_  z  \/  w  =  ~P z
) }  u.  ~P x )  i^i  ( tarskiMap `  X ) ) ) ,  { X }
)  |`  Y ) )
97 rdgfnon 6431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  rec (
( x  e.  _V  |->  ( ( { w  |  E. z  e.  x  ( w  C_  z  \/  w  =  ~P z
) }  u.  ~P x )  i^i  ( tarskiMap `  X ) ) ) ,  { X }
)  Fn  On
98 fnfun 5341 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( rec ( ( x  e. 
_V  |->  ( ( { w  |  E. z  e.  x  ( w  C_  z  \/  w  =  ~P z ) }  u.  ~P x )  i^i  ( tarskiMap `  X
) ) ) ,  { X } )  Fn  On  ->  Fun  rec ( ( x  e. 
_V  |->  ( ( { w  |  E. z  e.  x  ( w  C_  z  \/  w  =  ~P z ) }  u.  ~P x )  i^i  ( tarskiMap `  X
) ) ) ,  { X } ) )
99 funres 5293 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Fun 
rec ( ( x  e.  _V  |->  ( ( { w  |  E. z  e.  x  (
w  C_  z  \/  w  =  ~P z
) }  u.  ~P x )  i^i  ( tarskiMap `  X ) ) ) ,  { X }
)  ->  Fun  ( rec ( ( x  e. 
_V  |->  ( ( { w  |  E. z  e.  x  ( w  C_  z  \/  w  =  ~P z ) }  u.  ~P x )  i^i  ( tarskiMap `  X
) ) ) ,  { X } )  |`  Y ) )
10097, 98, 99mp2b 9 . . . . . . . . . . . . . . . . . . . . . 22  |-  Fun  ( rec ( ( x  e. 
_V  |->  ( ( { w  |  E. z  e.  x  ( w  C_  z  \/  w  =  ~P z ) }  u.  ~P x )  i^i  ( tarskiMap `  X
) ) ) ,  { X } )  |`  Y )
101 funeq 5274 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( tar `  <. X ,  Y >. )  =  ( rec ( ( x  e.  _V  |->  ( ( { w  |  E. z  e.  x  (
w  C_  z  \/  w  =  ~P z
) }  u.  ~P x )  i^i  ( tarskiMap `  X ) ) ) ,  { X }
)  |`  Y )  -> 
( Fun  ( tar ` 
<. X ,  Y >. )  <->  Fun  ( rec ( ( x  e.  _V  |->  ( ( { w  |  E. z  e.  x  ( w  C_  z  \/  w  =  ~P z
) }  u.  ~P x )  i^i  ( tarskiMap `  X ) ) ) ,  { X }
)  |`  Y ) ) )
102100, 101mpbiri 224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( tar `  <. X ,  Y >. )  =  ( rec ( ( x  e.  _V  |->  ( ( { w  |  E. z  e.  x  (
w  C_  z  \/  w  =  ~P z
) }  u.  ~P x )  i^i  ( tarskiMap `  X ) ) ) ,  { X }
)  |`  Y )  ->  Fun  ( tar `  <. X ,  Y >. )
)
10396, 102syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( X  e.  A  /\  Y  e.  On )  ->  Fun  ( tar `  <. X ,  Y >. )
)
1041033adant3 975 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  Fun  ( tar `  <. X ,  Y >. )
)
105104adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y ) )  ->  Fun  ( tar `  <. X ,  Y >. )
)
106 ordsuccl3 24516 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Y  e.  On  /\  suc  b  e.  Y
)  ->  b  C_  Y )
1071063adant1 973 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  b  C_  Y )
108 valdom 25296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( X  e.  A  /\  Y  e.  On )  ->  dom  ( tar `  <. X ,  Y >. )  =  Y )
1091083adant3 975 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  dom  ( tar `  <. X ,  Y >. )  =  Y )
110107, 109sseqtr4d 3215 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  b  C_  dom  ( tar `  <. X ,  Y >. ) )
111110adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y ) )  -> 
b  C_  dom  ( tar `  <. X ,  Y >. ) )
112105, 111jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y ) )  -> 
( Fun  ( tar ` 
<. X ,  Y >. )  /\  b  C_  dom  ( tar `  <. X ,  Y >. ) ) )
113112ex 423 . . . . . . . . . . . . . . . 16  |-  ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On )  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( Fun  ( tar `  <. X ,  Y >. )  /\  b  C_  dom  ( tar `  <. X ,  Y >. ) ) ) )
114 funimass4 5573 . . . . . . . . . . . . . . . . . 18  |-  ( ( Fun  ( tar `  <. X ,  Y >. )  /\  b  C_  dom  ( tar `  <. X ,  Y >. ) )  ->  (
( ( tar `  <. X ,  Y >. ) " b )  C_  ~P ( tarskiMap `  X )  <->  A. c  e.  b  ( ( tar `  <. X ,  Y >. ) `  c )  e.  ~P (
tarskiMap `
 X ) ) )
115 fvex 5539 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( tar `  <. X ,  Y >. ) `  c
)  e.  _V
116115elpw 3631 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( tar `  <. X ,  Y >. ) `  c )  e.  ~P (
tarskiMap `
 X )  <->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )
117116ralbii 2567 . . . . . . . . . . . . . . . . . 18  |-  ( A. c  e.  b  (
( tar `  <. X ,  Y >. ) `  c )  e.  ~P (
tarskiMap `
 X )  <->  A. c  e.  b  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )
118114, 117syl6bb 252 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  ( tar `  <. X ,  Y >. )  /\  b  C_  dom  ( tar `  <. X ,  Y >. ) )  ->  (
( ( tar `  <. X ,  Y >. ) " b )  C_  ~P ( tarskiMap `  X )  <->  A. c  e.  b  ( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) ) )
119 uniss 3848 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( tar `  <. X ,  Y >. ) " b )  C_  ~P ( tarskiMap `  X )  ->  U. ( ( tar `  <. X ,  Y >. ) " b ) 
C_  U. ~P ( tarskiMap `  X ) )
120 unipw 4224 . . . . . . . . . . . . . . . . . 18  |-  U. ~P (
tarskiMap `
 X )  =  ( tarskiMap `  X )
121119, 120syl6sseq 3224 . . . . . . . . . . . . . . . . 17  |-  ( ( ( tar `  <. X ,  Y >. ) " b )  C_  ~P ( tarskiMap `  X )  ->  U. ( ( tar `  <. X ,  Y >. ) " b ) 
C_  ( tarskiMap `  X
) )
122118, 121syl6bir 220 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  ( tar `  <. X ,  Y >. )  /\  b  C_  dom  ( tar `  <. X ,  Y >. ) )  ->  ( A. c  e.  b 
( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  ->  U. (
( tar `  <. X ,  Y >. ) " b )  C_  (
tarskiMap `
 X ) ) )
123113, 122syl6 29 . . . . . . . . . . . . . . 15  |-  ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On )  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  ( A. c  e.  b 
( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  ->  U. (
( tar `  <. X ,  Y >. ) " b )  C_  (
tarskiMap `
 X ) ) ) )
124123com23 72 . . . . . . . . . . . . . 14  |-  ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On )  ->  ( A. c  e.  b  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
)  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  U. ( ( tar `  <. X ,  Y >. ) " b ) 
C_  ( tarskiMap `  X
) ) ) )
12595, 124syl 15 . . . . . . . . . . . . 13  |-  ( A. c  e.  b  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  ( A. c  e.  b  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
)  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  U. ( ( tar `  <. X ,  Y >. ) " b ) 
C_  ( tarskiMap `  X
) ) ) )
126125impcom 419 . . . . . . . . . . . 12  |-  ( ( A. c  e.  b  ( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  /\  A. c  e.  b  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
)  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  U. ( ( tar `  <. X ,  Y >. ) " b ) 
C_  ( tarskiMap `  X
) ) )
12793, 126sylbi 187 . . . . . . . . . . 11  |-  ( A. c  e.  b  (
( ( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )
)  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  U. ( ( tar `  <. X ,  Y >. ) " b ) 
C_  ( tarskiMap `  X
) ) )
12862, 92, 1273syl 18 . . . . . . . . . 10  |-  ( ( A. c  e.  b  ( ( X  e.  A  /\  Y  e.  On  /\  suc  c  e.  Y )  ->  (
( tar `  <. X ,  Y >. ) `  c )  C_  ( tarskiMap `  X ) )  /\  ( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
) )  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  ->  U. (
( tar `  <. X ,  Y >. ) " b )  C_  (
tarskiMap `
 X ) ) )
129128ex 423 . . . . . . . . 9  |-  ( A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  ->  ( ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )  ->  U. ( ( tar `  <. X ,  Y >. ) " b ) 
C_  ( tarskiMap `  X
) ) ) )
130129pm2.43d 44 . . . . . . . 8  |-  ( A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  ->  U. (
( tar `  <. X ,  Y >. ) " b )  C_  (
tarskiMap `
 X ) ) )
131130a1i 10 . . . . . . 7  |-  ( Lim  b  ->  ( A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  ->  U. (
( tar `  <. X ,  Y >. ) " b )  C_  (
tarskiMap `
 X ) ) ) )
1321313imp 1145 . . . . . 6  |-  ( ( Lim  b  /\  A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  U. (
( tar `  <. X ,  Y >. ) " b )  C_  (
tarskiMap `
 X ) )
13361, 132eqsstrd 3212 . . . . 5  |-  ( ( Lim  b  /\  A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  /\  ( X  e.  A  /\  Y  e.  On  /\  suc  b  e.  Y )
)  ->  ( ( tar `  <. X ,  Y >. ) `  b ) 
C_  ( tarskiMap `  X
) )
1341333exp 1150 . . . 4  |-  ( Lim  b  ->  ( A. c  e.  b  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  c  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  c ) 
C_  ( tarskiMap `  X
) )  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  b  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  b ) 
C_  ( tarskiMap `  X
) ) ) )
1359, 15, 21, 27, 34, 51, 134tfinds 4650 . . 3  |-  ( B  e.  On  ->  (
( X  e.  A  /\  Y  e.  On  /\ 
suc  B  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  B ) 
C_  ( tarskiMap `  X
) ) )
1363, 135sylbir 204 . 2  |-  ( suc 
B  e.  On  ->  ( ( X  e.  A  /\  Y  e.  On  /\ 
suc  B  e.  Y
)  ->  ( ( tar `  <. X ,  Y >. ) `  B ) 
C_  ( tarskiMap `  X
) ) )
1372, 136mpcom 32 1  |-  ( ( X  e.  A  /\  Y  e.  On  /\  suc  B  e.  Y )  -> 
( ( tar `  <. X ,  Y >. ) `  B )  C_  ( tarskiMap `  X ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   {cab 2269    =/= wne 2446   A.wral 2543   E.wrex 2544   _Vcvv 2788    u. cun 3150    i^i cin 3151    C_ wss 3152   (/)c0 3455   ~Pcpw 3625   {csn 3640   <.cop 3643   U.cuni 3827    e. cmpt 4077   Tr wtr 4113   Ord word 4391   Oncon0 4392   Lim wlim 4393   suc csuc 4394   dom cdm 4689    |` cres 4691   "cima 4692   Fun wfun 5249    Fn wfn 5250   ` cfv 5255   reccrdg 6422   tarskiMapctskm 8459   tarctar 25293
This theorem is referenced by:  vtarsuelt  25307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-groth 8445
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-recs 6388  df-rdg 6423  df-tsk 8371  df-tskm 8460  df-tar 25294
  Copyright terms: Public domain W3C validator