Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexprlem1ssu Structured version   GIF version

Theorem recexprlem1ssu 6606
 Description: The upper cut of one is a subset of the upper cut of A ·P B. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
Assertion
Ref Expression
recexprlem1ssu (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem recexprlem1ssu
Dummy variables z w v u f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1pru 6537 . . . 4 (2nd ‘1P) = {w ∣ 1Q <Q w}
21abeq2i 2145 . . 3 (w (2nd ‘1P) ↔ 1Q <Q w)
3 prop 6458 . . . . . 6 (A P → ⟨(1stA), (2ndA)⟩ P)
4 prmuloc2 6548 . . . . . 6 ((⟨(1stA), (2ndA)⟩ P 1Q <Q w) → v (1stA)(v ·Q w) (2ndA))
53, 4sylan 267 . . . . 5 ((A P 1Q <Q w) → v (1stA)(v ·Q w) (2ndA))
6 prnminu 6472 . . . . . . . 8 ((⟨(1stA), (2ndA)⟩ P (v ·Q w) (2ndA)) → z (2ndA)z <Q (v ·Q w))
73, 6sylan 267 . . . . . . 7 ((A P (v ·Q w) (2ndA)) → z (2ndA)z <Q (v ·Q w))
87ad2ant2rl 480 . . . . . 6 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → z (2ndA)z <Q (v ·Q w))
9 simp3 905 . . . . . . . . . . 11 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → z <Q (v ·Q w))
10 simp2l 929 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → v (1stA))
11 elprnql 6464 . . . . . . . . . . . . . . . . . 18 ((⟨(1stA), (2ndA)⟩ P v (1stA)) → v Q)
123, 11sylan 267 . . . . . . . . . . . . . . . . 17 ((A P v (1stA)) → v Q)
1312ad2ant2r 478 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → v Q)
14133adant3 923 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → v Q)
15 simp1r 928 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → 1Q <Q w)
16 ltrelnq 6349 . . . . . . . . . . . . . . . . . 18 <Q ⊆ (Q × Q)
1716brel 4335 . . . . . . . . . . . . . . . . 17 (1Q <Q w → (1Q Q w Q))
1817simprd 107 . . . . . . . . . . . . . . . 16 (1Q <Q ww Q)
1915, 18syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → w Q)
20 recclnq 6376 . . . . . . . . . . . . . . . 16 (w Q → (*Qw) Q)
2119, 20syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Qw) Q)
22 mulassnqg 6368 . . . . . . . . . . . . . . 15 ((v Q w Q (*Qw) Q) → ((v ·Q w) ·Q (*Qw)) = (v ·Q (w ·Q (*Qw))))
2314, 19, 21, 22syl3anc 1134 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) = (v ·Q (w ·Q (*Qw))))
24 recidnq 6377 . . . . . . . . . . . . . . . 16 (w Q → (w ·Q (*Qw)) = 1Q)
2519, 24syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (w ·Q (*Qw)) = 1Q)
2625oveq2d 5471 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (v ·Q (w ·Q (*Qw))) = (v ·Q 1Q))
27 mulidnq 6373 . . . . . . . . . . . . . . 15 (v Q → (v ·Q 1Q) = v)
2814, 27syl 14 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (v ·Q 1Q) = v)
2923, 26, 283eqtrd 2073 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) = v)
3029eleq1d 2103 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((v ·Q w) ·Q (*Qw)) (1stA) ↔ v (1stA)))
3110, 30mpbird 156 . . . . . . . . . . 11 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) (1stA))
32 ltrnqi 6404 . . . . . . . . . . . . 13 (z <Q (v ·Q w) → (*Q‘(v ·Q w)) <Q (*Qz))
33 ltmnqg 6385 . . . . . . . . . . . . . . 15 ((f Q g Q Q) → (f <Q g ↔ ( ·Q f) <Q ( ·Q g)))
3433adantl 262 . . . . . . . . . . . . . 14 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q Q)) → (f <Q g ↔ ( ·Q f) <Q ( ·Q g)))
35 mulclnq 6360 . . . . . . . . . . . . . . . 16 ((v Q w Q) → (v ·Q w) Q)
3614, 19, 35syl2anc 391 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (v ·Q w) Q)
37 recclnq 6376 . . . . . . . . . . . . . . 15 ((v ·Q w) Q → (*Q‘(v ·Q w)) Q)
3836, 37syl 14 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Q‘(v ·Q w)) Q)
3916brel 4335 . . . . . . . . . . . . . . . . 17 (z <Q (v ·Q w) → (z Q (v ·Q w) Q))
4039simpld 105 . . . . . . . . . . . . . . . 16 (z <Q (v ·Q w) → z Q)
419, 40syl 14 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → z Q)
42 recclnq 6376 . . . . . . . . . . . . . . 15 (z Q → (*Qz) Q)
4341, 42syl 14 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Qz) Q)
44 mulcomnqg 6367 . . . . . . . . . . . . . . 15 ((f Q g Q) → (f ·Q g) = (g ·Q f))
4544adantl 262 . . . . . . . . . . . . . 14 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q)) → (f ·Q g) = (g ·Q f))
4634, 38, 43, 19, 45caovord2d 5612 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘(v ·Q w)) <Q (*Qz) ↔ ((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w)))
4732, 46syl5ib 143 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (z <Q (v ·Q w) → ((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w)))
48 1nq 6350 . . . . . . . . . . . . . . . . 17 1Q Q
49 mulidnq 6373 . . . . . . . . . . . . . . . . 17 (1Q Q → (1Q ·Q 1Q) = 1Q)
5048, 49ax-mp 7 . . . . . . . . . . . . . . . 16 (1Q ·Q 1Q) = 1Q
51 mulcomnqg 6367 . . . . . . . . . . . . . . . . . . . . 21 (((v ·Q w) Q (*Q‘(v ·Q w)) Q) → ((v ·Q w) ·Q (*Q‘(v ·Q w))) = ((*Q‘(v ·Q w)) ·Q (v ·Q w)))
5237, 51mpdan 398 . . . . . . . . . . . . . . . . . . . 20 ((v ·Q w) Q → ((v ·Q w) ·Q (*Q‘(v ·Q w))) = ((*Q‘(v ·Q w)) ·Q (v ·Q w)))
53 recidnq 6377 . . . . . . . . . . . . . . . . . . . 20 ((v ·Q w) Q → ((v ·Q w) ·Q (*Q‘(v ·Q w))) = 1Q)
5452, 53eqtr3d 2071 . . . . . . . . . . . . . . . . . . 19 ((v ·Q w) Q → ((*Q‘(v ·Q w)) ·Q (v ·Q w)) = 1Q)
5554, 24oveqan12d 5474 . . . . . . . . . . . . . . . . . 18 (((v ·Q w) Q w Q) → (((*Q‘(v ·Q w)) ·Q (v ·Q w)) ·Q (w ·Q (*Qw))) = (1Q ·Q 1Q))
5636, 19, 55syl2anc 391 . . . . . . . . . . . . . . . . 17 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((*Q‘(v ·Q w)) ·Q (v ·Q w)) ·Q (w ·Q (*Qw))) = (1Q ·Q 1Q))
57 mulassnqg 6368 . . . . . . . . . . . . . . . . . . 19 ((f Q g Q Q) → ((f ·Q g) ·Q ) = (f ·Q (g ·Q )))
5857adantl 262 . . . . . . . . . . . . . . . . . 18 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q Q)) → ((f ·Q g) ·Q ) = (f ·Q (g ·Q )))
59 mulclnq 6360 . . . . . . . . . . . . . . . . . . 19 ((f Q g Q) → (f ·Q g) Q)
6059adantl 262 . . . . . . . . . . . . . . . . . 18 ((((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) (f Q g Q)) → (f ·Q g) Q)
6138, 36, 19, 45, 58, 21, 60caov4d 5627 . . . . . . . . . . . . . . . . 17 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((*Q‘(v ·Q w)) ·Q (v ·Q w)) ·Q (w ·Q (*Qw))) = (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))))
6256, 61eqtr3d 2071 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (1Q ·Q 1Q) = (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))))
6350, 62syl5reqr 2084 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))) = 1Q)
6460, 38, 19caovcld 5596 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘(v ·Q w)) ·Q w) Q)
6560, 36, 21caovcld 5596 . . . . . . . . . . . . . . . 16 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((v ·Q w) ·Q (*Qw)) Q)
66 recmulnqg 6375 . . . . . . . . . . . . . . . 16 ((((*Q‘(v ·Q w)) ·Q w) Q ((v ·Q w) ·Q (*Qw)) Q) → ((*Q‘((*Q‘(v ·Q w)) ·Q w)) = ((v ·Q w) ·Q (*Qw)) ↔ (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))) = 1Q))
6764, 65, 66syl2anc 391 . . . . . . . . . . . . . . 15 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘((*Q‘(v ·Q w)) ·Q w)) = ((v ·Q w) ·Q (*Qw)) ↔ (((*Q‘(v ·Q w)) ·Q w) ·Q ((v ·Q w) ·Q (*Qw))) = 1Q))
6863, 67mpbird 156 . . . . . . . . . . . . . 14 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (*Q‘((*Q‘(v ·Q w)) ·Q w)) = ((v ·Q w) ·Q (*Qw)))
6968eleq1d 2103 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA) ↔ ((v ·Q w) ·Q (*Qw)) (1stA)))
7069biimprd 147 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → (((v ·Q w) ·Q (*Qw)) (1stA) → (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)))
71 breq1 3758 . . . . . . . . . . . . . . . 16 (y = ((*Q‘(v ·Q w)) ·Q w) → (y <Q ((*Qz) ·Q w) ↔ ((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w)))
72 fveq2 5121 . . . . . . . . . . . . . . . . 17 (y = ((*Q‘(v ·Q w)) ·Q w) → (*Qy) = (*Q‘((*Q‘(v ·Q w)) ·Q w)))
7372eleq1d 2103 . . . . . . . . . . . . . . . 16 (y = ((*Q‘(v ·Q w)) ·Q w) → ((*Qy) (1stA) ↔ (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)))
7471, 73anbi12d 442 . . . . . . . . . . . . . . 15 (y = ((*Q‘(v ·Q w)) ·Q w) → ((y <Q ((*Qz) ·Q w) (*Qy) (1stA)) ↔ (((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA))))
7574spcegv 2635 . . . . . . . . . . . . . 14 (((*Q‘(v ·Q w)) ·Q w) Q → ((((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)) → y(y <Q ((*Qz) ·Q w) (*Qy) (1stA))))
7664, 75syl 14 . . . . . . . . . . . . 13 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)) → y(y <Q ((*Qz) ·Q w) (*Qy) (1stA))))
77 recexpr.1 . . . . . . . . . . . . . 14 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
7877recexprlemelu 6595 . . . . . . . . . . . . 13 (((*Qz) ·Q w) (2ndB) ↔ y(y <Q ((*Qz) ·Q w) (*Qy) (1stA)))
7976, 78syl6ibr 151 . . . . . . . . . . . 12 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((((*Q‘(v ·Q w)) ·Q w) <Q ((*Qz) ·Q w) (*Q‘((*Q‘(v ·Q w)) ·Q w)) (1stA)) → ((*Qz) ·Q w) (2ndB)))
8047, 70, 79syl2and 279 . . . . . . . . . . 11 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((z <Q (v ·Q w) ((v ·Q w) ·Q (*Qw)) (1stA)) → ((*Qz) ·Q w) (2ndB)))
819, 31, 80mp2and 409 . . . . . . . . . 10 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → ((*Qz) ·Q w) (2ndB))
82 mulidnq 6373 . . . . . . . . . . . . . 14 (w Q → (w ·Q 1Q) = w)
83 mulcomnqg 6367 . . . . . . . . . . . . . . 15 ((w Q 1Q Q) → (w ·Q 1Q) = (1Q ·Q w))
8448, 83mpan2 401 . . . . . . . . . . . . . 14 (w Q → (w ·Q 1Q) = (1Q ·Q w))
8582, 84eqtr3d 2071 . . . . . . . . . . . . 13 (w Qw = (1Q ·Q w))
8685adantl 262 . . . . . . . . . . . 12 ((z Q w Q) → w = (1Q ·Q w))
87 recidnq 6377 . . . . . . . . . . . . . 14 (z Q → (z ·Q (*Qz)) = 1Q)
8887oveq1d 5470 . . . . . . . . . . . . 13 (z Q → ((z ·Q (*Qz)) ·Q w) = (1Q ·Q w))
8988adantr 261 . . . . . . . . . . . 12 ((z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (1Q ·Q w))
90 mulassnqg 6368 . . . . . . . . . . . . . 14 ((z Q (*Qz) Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9142, 90syl3an2 1168 . . . . . . . . . . . . 13 ((z Q z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
92913anidm12 1191 . . . . . . . . . . . 12 ((z Q w Q) → ((z ·Q (*Qz)) ·Q w) = (z ·Q ((*Qz) ·Q w)))
9386, 89, 923eqtr2d 2075 . . . . . . . . . . 11 ((z Q w Q) → w = (z ·Q ((*Qz) ·Q w)))
9441, 19, 93syl2anc 391 . . . . . . . . . 10 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → w = (z ·Q ((*Qz) ·Q w)))
95 oveq2 5463 . . . . . . . . . . . 12 (x = ((*Qz) ·Q w) → (z ·Q x) = (z ·Q ((*Qz) ·Q w)))
9695eqeq2d 2048 . . . . . . . . . . 11 (x = ((*Qz) ·Q w) → (w = (z ·Q x) ↔ w = (z ·Q ((*Qz) ·Q w))))
9796rspcev 2650 . . . . . . . . . 10 ((((*Qz) ·Q w) (2ndB) w = (z ·Q ((*Qz) ·Q w))) → x (2ndB)w = (z ·Q x))
9881, 94, 97syl2anc 391 . . . . . . . . 9 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA)) z <Q (v ·Q w)) → x (2ndB)w = (z ·Q x))
99983expia 1105 . . . . . . . 8 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (z <Q (v ·Q w) → x (2ndB)w = (z ·Q x)))
10099reximdv 2414 . . . . . . 7 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (z (2ndA)z <Q (v ·Q w) → z (2ndA)x (2ndB)w = (z ·Q x)))
10177recexprlempr 6604 . . . . . . . . 9 (A PB P)
102 df-imp 6452 . . . . . . . . . 10 ·P = (y P, w P ↦ ⟨{u Qf Q g Q (f (1sty) g (1stw) u = (f ·Q g))}, {u Qf Q g Q (f (2ndy) g (2ndw) u = (f ·Q g))}⟩)
103102, 59genpelvu 6496 . . . . . . . . 9 ((A P B P) → (w (2nd ‘(A ·P B)) ↔ z (2ndA)x (2ndB)w = (z ·Q x)))
104101, 103mpdan 398 . . . . . . . 8 (A P → (w (2nd ‘(A ·P B)) ↔ z (2ndA)x (2ndB)w = (z ·Q x)))
105104ad2antrr 457 . . . . . . 7 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (w (2nd ‘(A ·P B)) ↔ z (2ndA)x (2ndB)w = (z ·Q x)))
106100, 105sylibrd 158 . . . . . 6 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → (z (2ndA)z <Q (v ·Q w) → w (2nd ‘(A ·P B))))
1078, 106mpd 13 . . . . 5 (((A P 1Q <Q w) (v (1stA) (v ·Q w) (2ndA))) → w (2nd ‘(A ·P B)))
1085, 107rexlimddv 2431 . . . 4 ((A P 1Q <Q w) → w (2nd ‘(A ·P B)))
109108ex 108 . . 3 (A P → (1Q <Q ww (2nd ‘(A ·P B))))
1102, 109syl5bi 141 . 2 (A P → (w (2nd ‘1P) → w (2nd ‘(A ·P B))))
111110ssrdv 2945 1 (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  ∃wrex 2301   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264  1Qc1q 6265   ·Q cmq 6267  *Qcrq 6268
 Copyright terms: Public domain W3C validator