Metamath Proof Explorer

Theorem no3indslem

Description: Triple induction over surreal numbers. Lemma with explicit relationship. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses no3indslem.a 
|- R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
no3indslem.b 
|- S = { <. c , d >. | ( c e. ( ( No X. No ) X. No ) /\ d e. ( ( No X. No ) X. No ) /\ ( ( ( ( 1st ` ( 1st ` c ) ) R ( 1st ` ( 1st ` d ) ) \/ ( 1st ` ( 1st ` c ) ) = ( 1st ` ( 1st ` d ) ) ) /\ ( ( 2nd ` ( 1st ` c ) ) R ( 2nd ` ( 1st ` d ) ) \/ ( 2nd ` ( 1st ` c ) ) = ( 2nd ` ( 1st ` d ) ) ) /\ ( ( 2nd ` c ) R ( 2nd ` d ) \/ ( 2nd ` c ) = ( 2nd ` d ) ) ) /\ c =/= d ) ) }
no3indslem.1 
|- ( p = q -> ( ph <-> ps ) )
no3indslem.2 
|- ( p = <. <. x , y >. , z >. -> ( ph <-> ch ) )
no3indslem.3 
|- ( q = <. <. w , t >. , u >. -> ( ps <-> th ) )
no3indslem.4 
|- ( u = z -> ( th <-> ta ) )
no3indslem.5 
|- ( t = y -> ( th <-> et ) )
no3indslem.6 
|- ( u = z -> ( et <-> ze ) )
no3indslem.7 
|- ( w = x -> ( th <-> si ) )
no3indslem.8 
|- ( u = z -> ( si <-> rh ) )
no3indslem.9 
|- ( t = y -> ( si <-> mu ) )
no3indslem.10 
|- ( x = A -> ( ch <-> la ) )
no3indslem.11 
|- ( y = B -> ( la <-> ka ) )
no3indslem.12 
|- ( z = C -> ( ka <-> al ) )
no3indslem.i 
|- ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) /\ ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) /\ A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu ) -> ch ) )
Assertion no3indslem 
|- ( ( A e. No /\ B e. No /\ C e. No ) -> al )

Proof

Step Hyp Ref Expression
1 no3indslem.a 
 |-  R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
2 no3indslem.b 
 |-  S = { <. c , d >. | ( c e. ( ( No X. No ) X. No ) /\ d e. ( ( No X. No ) X. No ) /\ ( ( ( ( 1st ` ( 1st ` c ) ) R ( 1st ` ( 1st ` d ) ) \/ ( 1st ` ( 1st ` c ) ) = ( 1st ` ( 1st ` d ) ) ) /\ ( ( 2nd ` ( 1st ` c ) ) R ( 2nd ` ( 1st ` d ) ) \/ ( 2nd ` ( 1st ` c ) ) = ( 2nd ` ( 1st ` d ) ) ) /\ ( ( 2nd ` c ) R ( 2nd ` d ) \/ ( 2nd ` c ) = ( 2nd ` d ) ) ) /\ c =/= d ) ) }
3 no3indslem.1 
 |-  ( p = q -> ( ph <-> ps ) )
4 no3indslem.2 
 |-  ( p = <. <. x , y >. , z >. -> ( ph <-> ch ) )
5 no3indslem.3 
 |-  ( q = <. <. w , t >. , u >. -> ( ps <-> th ) )
6 no3indslem.4 
 |-  ( u = z -> ( th <-> ta ) )
7 no3indslem.5 
 |-  ( t = y -> ( th <-> et ) )
8 no3indslem.6 
 |-  ( u = z -> ( et <-> ze ) )
9 no3indslem.7 
 |-  ( w = x -> ( th <-> si ) )
10 no3indslem.8 
 |-  ( u = z -> ( si <-> rh ) )
11 no3indslem.9 
 |-  ( t = y -> ( si <-> mu ) )
12 no3indslem.10 
 |-  ( x = A -> ( ch <-> la ) )
13 no3indslem.11 
 |-  ( y = B -> ( la <-> ka ) )
14 no3indslem.12 
 |-  ( z = C -> ( ka <-> al ) )
15 no3indslem.i 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) /\ ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) /\ A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu ) -> ch ) )
16 1 lrrecfr 
 |-  R Fr No
17 16 a1i 
 |-  ( T. -> R Fr No )
18 2 17 17 17 frxp3 
 |-  ( T. -> S Fr ( ( No X. No ) X. No ) )
19 18 mptru 
 |-  S Fr ( ( No X. No ) X. No )
20 1 lrrecpo 
 |-  R Po No
21 20 a1i 
 |-  ( T. -> R Po No )
22 2 21 21 21 poxp3 
 |-  ( T. -> S Po ( ( No X. No ) X. No ) )
23 22 mptru 
 |-  S Po ( ( No X. No ) X. No )
24 1 lrrecse 
 |-  R Se No
25 24 a1i 
 |-  ( T. -> R Se No )
26 2 25 25 25 sexp3 
 |-  ( T. -> S Se ( ( No X. No ) X. No ) )
27 26 mptru 
 |-  S Se ( ( No X. No ) X. No )
28 elxpxp 
 |-  ( p e. ( ( No X. No ) X. No ) <-> E. x e. No E. y e. No E. z e. No p = <. <. x , y >. , z >. )
29 2 xpord3pred 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) = ( ( ( ( Pred ( R , No , x ) u. { x } ) X. ( Pred ( R , No , y ) u. { y } ) ) X. ( Pred ( R , No , z ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) )
30 1 lrrecpred 
 |-  ( x e. No -> Pred ( R , No , x ) = ( ( _L ` x ) u. ( _R ` x ) ) )
31 30 3ad2ant1 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> Pred ( R , No , x ) = ( ( _L ` x ) u. ( _R ` x ) ) )
32 31 uneq1d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( Pred ( R , No , x ) u. { x } ) = ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) )
33 1 lrrecpred 
 |-  ( y e. No -> Pred ( R , No , y ) = ( ( _L ` y ) u. ( _R ` y ) ) )
34 33 3ad2ant2 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> Pred ( R , No , y ) = ( ( _L ` y ) u. ( _R ` y ) ) )
35 34 uneq1d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( Pred ( R , No , y ) u. { y } ) = ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) )
36 32 35 xpeq12d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( Pred ( R , No , x ) u. { x } ) X. ( Pred ( R , No , y ) u. { y } ) ) = ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) )
37 1 lrrecpred 
 |-  ( z e. No -> Pred ( R , No , z ) = ( ( _L ` z ) u. ( _R ` z ) ) )
38 37 3ad2ant3 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> Pred ( R , No , z ) = ( ( _L ` z ) u. ( _R ` z ) ) )
39 38 uneq1d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( Pred ( R , No , z ) u. { z } ) = ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) )
40 36 39 xpeq12d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( Pred ( R , No , x ) u. { x } ) X. ( Pred ( R , No , y ) u. { y } ) ) X. ( Pred ( R , No , z ) u. { z } ) ) = ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) )
41 40 difeq1d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( ( Pred ( R , No , x ) u. { x } ) X. ( Pred ( R , No , y ) u. { y } ) ) X. ( Pred ( R , No , z ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) = ( ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) )
42 29 41 eqtrd 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) = ( ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) )
43 42 raleqdv 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) ps <-> A. q e. ( ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) ps ) )
44 eldif 
 |-  ( q e. ( ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) <-> ( q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) /\ -. q e. { <. <. x , y >. , z >. } ) )
45 44 imbi1i 
 |-  ( ( q e. ( ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) -> ps ) <-> ( ( q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) /\ -. q e. { <. <. x , y >. , z >. } ) -> ps ) )
46 impexp 
 |-  ( ( ( q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) /\ -. q e. { <. <. x , y >. , z >. } ) -> ps ) <-> ( q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) -> ( -. q e. { <. <. x , y >. , z >. } -> ps ) ) )
47 45 46 bitri 
 |-  ( ( q e. ( ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) -> ps ) <-> ( q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) -> ( -. q e. { <. <. x , y >. , z >. } -> ps ) ) )
48 47 ralbii2 
 |-  ( A. q e. ( ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) \ { <. <. x , y >. , z >. } ) ps <-> A. q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) ( -. q e. { <. <. x , y >. , z >. } -> ps ) )
49 43 48 bitrdi 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) ps <-> A. q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) ( -. q e. { <. <. x , y >. , z >. } -> ps ) ) )
50 eleq1 
 |-  ( q = <. <. w , t >. , u >. -> ( q e. { <. <. x , y >. , z >. } <-> <. <. w , t >. , u >. e. { <. <. x , y >. , z >. } ) )
51 50 notbid 
 |-  ( q = <. <. w , t >. , u >. -> ( -. q e. { <. <. x , y >. , z >. } <-> -. <. <. w , t >. , u >. e. { <. <. x , y >. , z >. } ) )
52 df-ne 
 |-  ( <. <. w , t >. , u >. =/= <. <. x , y >. , z >. <-> -. <. <. w , t >. , u >. = <. <. x , y >. , z >. )
53 vex 
 |-  w e. _V
54 vex 
 |-  t e. _V
55 vex 
 |-  u e. _V
56 53 54 55 otthne 
 |-  ( <. <. w , t >. , u >. =/= <. <. x , y >. , z >. <-> ( w =/= x \/ t =/= y \/ u =/= z ) )
57 52 56 bitr3i 
 |-  ( -. <. <. w , t >. , u >. = <. <. x , y >. , z >. <-> ( w =/= x \/ t =/= y \/ u =/= z ) )
58 opex 
 |-  <. <. w , t >. , u >. e. _V
59 58 elsn 
 |-  ( <. <. w , t >. , u >. e. { <. <. x , y >. , z >. } <-> <. <. w , t >. , u >. = <. <. x , y >. , z >. )
60 57 59 xchnxbir 
 |-  ( -. <. <. w , t >. , u >. e. { <. <. x , y >. , z >. } <-> ( w =/= x \/ t =/= y \/ u =/= z ) )
61 51 60 bitrdi 
 |-  ( q = <. <. w , t >. , u >. -> ( -. q e. { <. <. x , y >. , z >. } <-> ( w =/= x \/ t =/= y \/ u =/= z ) ) )
62 61 5 imbi12d 
 |-  ( q = <. <. w , t >. , u >. -> ( ( -. q e. { <. <. x , y >. , z >. } -> ps ) <-> ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) )
63 62 ralxp3 
 |-  ( A. q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) ( -. q e. { <. <. x , y >. , z >. } -> ps ) <-> A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
64 ssun1 
 |-  ( ( _L ` x ) u. ( _R ` x ) ) C_ ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } )
65 ssralv 
 |-  ( ( ( _L ` x ) u. ( _R ` x ) ) C_ ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) -> ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) )
66 64 65 ax-mp 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
67 ssun1 
 |-  ( ( _L ` y ) u. ( _R ` y ) ) C_ ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } )
68 ssralv 
 |-  ( ( ( _L ` y ) u. ( _R ` y ) ) C_ ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) -> ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) )
69 67 68 ax-mp 
 |-  ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
70 ssun1 
 |-  ( ( _L ` z ) u. ( _R ` z ) ) C_ ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } )
71 ssralv 
 |-  ( ( ( _L ` z ) u. ( _R ` z ) ) C_ ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) -> ( A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) )
72 70 71 ax-mp 
 |-  ( A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
73 72 ralimi 
 |-  ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
74 69 73 syl 
 |-  ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
75 74 ralimi 
 |-  ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
76 66 75 syl 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
77 76 adantl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
78 nfv 
 |-  F/ w ( x e. No /\ y e. No /\ z e. No )
79 nfra1 
 |-  F/ w A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th )
80 78 79 nfan 
 |-  F/ w ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
81 nfv 
 |-  F/ t ( x e. No /\ y e. No /\ z e. No )
82 nfra2w 
 |-  F/ t A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th )
83 81 82 nfan 
 |-  F/ t ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
84 nfv 
 |-  F/ t w e. ( ( _L ` x ) u. ( _R ` x ) )
85 83 84 nfan 
 |-  F/ t ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) )
86 nfv 
 |-  F/ u ( x e. No /\ y e. No /\ z e. No )
87 nfcv 
 |-  F/_ u ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } )
88 nfra2w 
 |-  F/ u A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th )
89 87 88 nfralw 
 |-  F/ u A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th )
90 86 89 nfan 
 |-  F/ u ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
91 nfv 
 |-  F/ u w e. ( ( _L ` x ) u. ( _R ` x ) )
92 90 91 nfan 
 |-  F/ u ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) )
93 nfv 
 |-  F/ u t e. ( ( _L ` y ) u. ( _R ` y ) )
94 92 93 nfan 
 |-  F/ u ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) )
95 simpl1 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> x e. No )
96 leftirr 
 |-  ( x e. No -> -. x e. ( _L ` x ) )
97 95 96 syl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. x e. ( _L ` x ) )
98 rightirr 
 |-  ( x e. No -> -. x e. ( _R ` x ) )
99 95 98 syl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. x e. ( _R ` x ) )
100 ioran 
 |-  ( -. ( x e. ( _L ` x ) \/ x e. ( _R ` x ) ) <-> ( -. x e. ( _L ` x ) /\ -. x e. ( _R ` x ) ) )
101 97 99 100 sylanbrc 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. ( x e. ( _L ` x ) \/ x e. ( _R ` x ) ) )
102 eleq1w 
 |-  ( w = x -> ( w e. ( ( _L ` x ) u. ( _R ` x ) ) <-> x e. ( ( _L ` x ) u. ( _R ` x ) ) ) )
103 elun 
 |-  ( x e. ( ( _L ` x ) u. ( _R ` x ) ) <-> ( x e. ( _L ` x ) \/ x e. ( _R ` x ) ) )
104 102 103 bitrdi 
 |-  ( w = x -> ( w e. ( ( _L ` x ) u. ( _R ` x ) ) <-> ( x e. ( _L ` x ) \/ x e. ( _R ` x ) ) ) )
105 104 notbid 
 |-  ( w = x -> ( -. w e. ( ( _L ` x ) u. ( _R ` x ) ) <-> -. ( x e. ( _L ` x ) \/ x e. ( _R ` x ) ) ) )
106 101 105 syl5ibrcom 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( w = x -> -. w e. ( ( _L ` x ) u. ( _R ` x ) ) ) )
107 106 necon2ad 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( w e. ( ( _L ` x ) u. ( _R ` x ) ) -> w =/= x ) )
108 107 imp 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> w =/= x )
109 108 3mix1d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( w =/= x \/ t =/= y \/ u =/= z ) )
110 109 adantr 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( w =/= x \/ t =/= y \/ u =/= z ) )
111 110 adantr 
 |-  ( ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( w =/= x \/ t =/= y \/ u =/= z ) )
112 pm2.27 
 |-  ( ( w =/= x \/ t =/= y \/ u =/= z ) -> ( ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> th ) )
113 111 112 syl 
 |-  ( ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> th ) )
114 94 113 ralimda 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th ) )
115 85 114 ralimda 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th ) )
116 80 115 ralimda 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th ) )
117 77 116 mpd 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th )
118 ssun2 
 |-  { z } C_ ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } )
119 ssralv 
 |-  ( { z } C_ ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) -> ( A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) )
120 118 119 ax-mp 
 |-  ( A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
121 120 ralimi 
 |-  ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
122 69 121 syl 
 |-  ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
123 122 ralimi 
 |-  ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
124 66 123 syl 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
125 124 adantl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
126 vex 
 |-  z e. _V
127 biidd 
 |-  ( u = z -> ( w =/= x <-> w =/= x ) )
128 biidd 
 |-  ( u = z -> ( t =/= y <-> t =/= y ) )
129 neeq1 
 |-  ( u = z -> ( u =/= z <-> z =/= z ) )
130 127 128 129 3orbi123d 
 |-  ( u = z -> ( ( w =/= x \/ t =/= y \/ u =/= z ) <-> ( w =/= x \/ t =/= y \/ z =/= z ) ) )
131 130 6 imbi12d 
 |-  ( u = z -> ( ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) ) )
132 126 131 ralsn 
 |-  ( A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) )
133 132 2ralbii 
 |-  ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) )
134 125 133 sylib 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) )
135 108 3mix1d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( w =/= x \/ t =/= y \/ z =/= z ) )
136 135 adantr 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( w =/= x \/ t =/= y \/ z =/= z ) )
137 pm2.27 
 |-  ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ( ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) -> ta ) )
138 136 137 syl 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) -> ta ) )
139 85 138 ralimda 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta ) )
140 80 139 ralimda 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( w =/= x \/ t =/= y \/ z =/= z ) -> ta ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta ) )
141 134 140 mpd 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta )
142 ssun2 
 |-  { y } C_ ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } )
143 ssralv 
 |-  ( { y } C_ ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) -> ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. { y } A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) )
144 142 143 ax-mp 
 |-  ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. { y } A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
145 72 ralimi 
 |-  ( A. t e. { y } A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
146 144 145 syl 
 |-  ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
147 146 ralimi 
 |-  ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
148 66 147 syl 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
149 148 adantl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
150 vex 
 |-  y e. _V
151 biidd 
 |-  ( t = y -> ( w =/= x <-> w =/= x ) )
152 neeq1 
 |-  ( t = y -> ( t =/= y <-> y =/= y ) )
153 biidd 
 |-  ( t = y -> ( u =/= z <-> u =/= z ) )
154 151 152 153 3orbi123d 
 |-  ( t = y -> ( ( w =/= x \/ t =/= y \/ u =/= z ) <-> ( w =/= x \/ y =/= y \/ u =/= z ) ) )
155 154 7 imbi12d 
 |-  ( t = y -> ( ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) ) )
156 155 ralbidv 
 |-  ( t = y -> ( A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) ) )
157 150 156 ralsn 
 |-  ( A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) )
158 157 ralbii 
 |-  ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) )
159 149 158 sylib 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) )
160 108 3mix1d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( w =/= x \/ y =/= y \/ u =/= z ) )
161 160 adantr 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( w =/= x \/ y =/= y \/ u =/= z ) )
162 pm2.27 
 |-  ( ( w =/= x \/ y =/= y \/ u =/= z ) -> ( ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) -> et ) )
163 161 162 syl 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) -> et ) )
164 92 163 ralimda 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) )
165 80 164 ralimda 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) )
166 159 165 mpd 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et )
167 117 141 166 3jca 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) )
168 120 ralimi 
 |-  ( A. t e. { y } A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
169 144 168 syl 
 |-  ( A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
170 169 ralimi 
 |-  ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
171 66 170 syl 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
172 171 adantl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
173 155 ralbidv 
 |-  ( t = y -> ( A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. u e. { z } ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) ) )
174 150 173 ralsn 
 |-  ( A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. u e. { z } ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) )
175 biidd 
 |-  ( u = z -> ( y =/= y <-> y =/= y ) )
176 127 175 129 3orbi123d 
 |-  ( u = z -> ( ( w =/= x \/ y =/= y \/ u =/= z ) <-> ( w =/= x \/ y =/= y \/ z =/= z ) ) )
177 176 8 imbi12d 
 |-  ( u = z -> ( ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) <-> ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) ) )
178 126 177 ralsn 
 |-  ( A. u e. { z } ( ( w =/= x \/ y =/= y \/ u =/= z ) -> et ) <-> ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) )
179 174 178 bitri 
 |-  ( A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) )
180 179 ralbii 
 |-  ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. { y } A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) )
181 172 180 sylib 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) )
182 108 3mix1d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( w =/= x \/ y =/= y \/ z =/= z ) )
183 pm2.27 
 |-  ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ( ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) -> ze ) )
184 182 183 syl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ w e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) -> ze ) )
185 80 184 ralimda 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ( ( w =/= x \/ y =/= y \/ z =/= z ) -> ze ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze ) )
186 181 185 mpd 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze )
187 ssun2 
 |-  { x } C_ ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } )
188 ssralv 
 |-  ( { x } C_ ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) -> ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) )
189 187 188 ax-mp 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
190 74 ralimi 
 |-  ( A. w e. { x } A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
191 189 190 syl 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
192 191 adantl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
193 vex 
 |-  x e. _V
194 neeq1 
 |-  ( w = x -> ( w =/= x <-> x =/= x ) )
195 biidd 
 |-  ( w = x -> ( t =/= y <-> t =/= y ) )
196 biidd 
 |-  ( w = x -> ( u =/= z <-> u =/= z ) )
197 194 195 196 3orbi123d 
 |-  ( w = x -> ( ( w =/= x \/ t =/= y \/ u =/= z ) <-> ( x =/= x \/ t =/= y \/ u =/= z ) ) )
198 197 9 imbi12d 
 |-  ( w = x -> ( ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) ) )
199 198 2ralbidv 
 |-  ( w = x -> ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) ) )
200 193 199 ralsn 
 |-  ( A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) )
201 192 200 sylib 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) )
202 90 93 nfan 
 |-  F/ u ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) )
203 simpl2 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> y e. No )
204 leftirr 
 |-  ( y e. No -> -. y e. ( _L ` y ) )
205 203 204 syl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. y e. ( _L ` y ) )
206 rightirr 
 |-  ( y e. No -> -. y e. ( _R ` y ) )
207 203 206 syl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. y e. ( _R ` y ) )
208 ioran 
 |-  ( -. ( y e. ( _L ` y ) \/ y e. ( _R ` y ) ) <-> ( -. y e. ( _L ` y ) /\ -. y e. ( _R ` y ) ) )
209 205 207 208 sylanbrc 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. ( y e. ( _L ` y ) \/ y e. ( _R ` y ) ) )
210 eleq1w 
 |-  ( t = y -> ( t e. ( ( _L ` y ) u. ( _R ` y ) ) <-> y e. ( ( _L ` y ) u. ( _R ` y ) ) ) )
211 elun 
 |-  ( y e. ( ( _L ` y ) u. ( _R ` y ) ) <-> ( y e. ( _L ` y ) \/ y e. ( _R ` y ) ) )
212 210 211 bitrdi 
 |-  ( t = y -> ( t e. ( ( _L ` y ) u. ( _R ` y ) ) <-> ( y e. ( _L ` y ) \/ y e. ( _R ` y ) ) ) )
213 212 notbid 
 |-  ( t = y -> ( -. t e. ( ( _L ` y ) u. ( _R ` y ) ) <-> -. ( y e. ( _L ` y ) \/ y e. ( _R ` y ) ) ) )
214 209 213 syl5ibrcom 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( t = y -> -. t e. ( ( _L ` y ) u. ( _R ` y ) ) ) )
215 214 necon2ad 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( t e. ( ( _L ` y ) u. ( _R ` y ) ) -> t =/= y ) )
216 215 imp 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> t =/= y )
217 216 adantr 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> t =/= y )
218 217 3mix2d 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( x =/= x \/ t =/= y \/ u =/= z ) )
219 pm2.27 
 |-  ( ( x =/= x \/ t =/= y \/ u =/= z ) -> ( ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) -> si ) )
220 218 219 syl 
 |-  ( ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) -> si ) )
221 202 220 ralimda 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si ) )
222 83 221 ralimda 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si ) )
223 201 222 mpd 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si )
224 122 ralimi 
 |-  ( A. w e. { x } A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
225 189 224 syl 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
226 225 adantl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
227 198 2ralbidv 
 |-  ( w = x -> ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) ) )
228 193 227 ralsn 
 |-  ( A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) )
229 biidd 
 |-  ( u = z -> ( x =/= x <-> x =/= x ) )
230 229 128 129 3orbi123d 
 |-  ( u = z -> ( ( x =/= x \/ t =/= y \/ u =/= z ) <-> ( x =/= x \/ t =/= y \/ z =/= z ) ) )
231 230 10 imbi12d 
 |-  ( u = z -> ( ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) <-> ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) ) )
232 126 231 ralsn 
 |-  ( A. u e. { z } ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) <-> ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) )
233 232 ralbii 
 |-  ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) <-> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) )
234 228 233 bitri 
 |-  ( A. w e. { x } A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. { z } ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) )
235 226 234 sylib 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) )
236 216 3mix2d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( x =/= x \/ t =/= y \/ z =/= z ) )
237 pm2.27 
 |-  ( ( x =/= x \/ t =/= y \/ z =/= z ) -> ( ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) -> rh ) )
238 236 237 syl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ t e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) -> rh ) )
239 83 238 ralimda 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ( ( x =/= x \/ t =/= y \/ z =/= z ) -> rh ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) )
240 235 239 mpd 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh )
241 186 223 240 3jca 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) )
242 146 ralimi 
 |-  ( A. w e. { x } A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
243 189 242 syl 
 |-  ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> A. w e. { x } A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
244 243 adantl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. w e. { x } A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) )
245 198 2ralbidv 
 |-  ( w = x -> ( A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) ) )
246 193 245 ralsn 
 |-  ( A. w e. { x } A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) )
247 biidd 
 |-  ( t = y -> ( x =/= x <-> x =/= x ) )
248 247 152 153 3orbi123d 
 |-  ( t = y -> ( ( x =/= x \/ t =/= y \/ u =/= z ) <-> ( x =/= x \/ y =/= y \/ u =/= z ) ) )
249 248 11 imbi12d 
 |-  ( t = y -> ( ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) <-> ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) ) )
250 249 ralbidv 
 |-  ( t = y -> ( A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) <-> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) ) )
251 150 250 ralsn 
 |-  ( A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ t =/= y \/ u =/= z ) -> si ) <-> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) )
252 246 251 bitri 
 |-  ( A. w e. { x } A. t e. { y } A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) <-> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) )
253 244 252 sylib 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) )
254 simpl3 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> z e. No )
255 leftirr 
 |-  ( z e. No -> -. z e. ( _L ` z ) )
256 254 255 syl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. z e. ( _L ` z ) )
257 rightirr 
 |-  ( z e. No -> -. z e. ( _R ` z ) )
258 254 257 syl 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. z e. ( _R ` z ) )
259 ioran 
 |-  ( -. ( z e. ( _L ` z ) \/ z e. ( _R ` z ) ) <-> ( -. z e. ( _L ` z ) /\ -. z e. ( _R ` z ) ) )
260 256 258 259 sylanbrc 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> -. ( z e. ( _L ` z ) \/ z e. ( _R ` z ) ) )
261 eleq1w 
 |-  ( u = z -> ( u e. ( ( _L ` z ) u. ( _R ` z ) ) <-> z e. ( ( _L ` z ) u. ( _R ` z ) ) ) )
262 elun 
 |-  ( z e. ( ( _L ` z ) u. ( _R ` z ) ) <-> ( z e. ( _L ` z ) \/ z e. ( _R ` z ) ) )
263 261 262 bitrdi 
 |-  ( u = z -> ( u e. ( ( _L ` z ) u. ( _R ` z ) ) <-> ( z e. ( _L ` z ) \/ z e. ( _R ` z ) ) ) )
264 263 notbid 
 |-  ( u = z -> ( -. u e. ( ( _L ` z ) u. ( _R ` z ) ) <-> -. ( z e. ( _L ` z ) \/ z e. ( _R ` z ) ) ) )
265 260 264 syl5ibrcom 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( u = z -> -. u e. ( ( _L ` z ) u. ( _R ` z ) ) ) )
266 265 necon2ad 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( u e. ( ( _L ` z ) u. ( _R ` z ) ) -> u =/= z ) )
267 266 imp 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> u =/= z )
268 267 3mix3d 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( x =/= x \/ y =/= y \/ u =/= z ) )
269 pm2.27 
 |-  ( ( x =/= x \/ y =/= y \/ u =/= z ) -> ( ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) -> mu ) )
270 268 269 syl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) /\ u e. ( ( _L ` z ) u. ( _R ` z ) ) ) -> ( ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) -> mu ) )
271 90 270 ralimda 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( A. u e. ( ( _L ` z ) u. ( _R ` z ) ) ( ( x =/= x \/ y =/= y \/ u =/= z ) -> mu ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu ) )
272 253 271 mpd 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu )
273 167 241 272 3jca 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) ) -> ( ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) /\ ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) /\ A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu ) )
274 273 ex 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> ( ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) th /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. t e. ( ( _L ` y ) u. ( _R ` y ) ) ta /\ A. w e. ( ( _L ` x ) u. ( _R ` x ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) et ) /\ ( A. w e. ( ( _L ` x ) u. ( _R ` x ) ) ze /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) A. u e. ( ( _L ` z ) u. ( _R ` z ) ) si /\ A. t e. ( ( _L ` y ) u. ( _R ` y ) ) rh ) /\ A. u e. ( ( _L ` z ) u. ( _R ` z ) ) mu ) ) )
275 274 15 syld 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( A. w e. ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) A. t e. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) A. u e. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ( ( w =/= x \/ t =/= y \/ u =/= z ) -> th ) -> ch ) )
276 63 275 syl5bi 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( A. q e. ( ( ( ( ( _L ` x ) u. ( _R ` x ) ) u. { x } ) X. ( ( ( _L ` y ) u. ( _R ` y ) ) u. { y } ) ) X. ( ( ( _L ` z ) u. ( _R ` z ) ) u. { z } ) ) ( -. q e. { <. <. x , y >. , z >. } -> ps ) -> ch ) )
277 49 276 sylbid 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) ps -> ch ) )
278 predeq3 
 |-  ( p = <. <. x , y >. , z >. -> Pred ( S , ( ( No X. No ) X. No ) , p ) = Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) )
279 278 raleqdv 
 |-  ( p = <. <. x , y >. , z >. -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , p ) ps <-> A. q e. Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) ps ) )
280 279 4 imbi12d 
 |-  ( p = <. <. x , y >. , z >. -> ( ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , p ) ps -> ph ) <-> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , <. <. x , y >. , z >. ) ps -> ch ) ) )
281 277 280 syl5ibrcom 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( p = <. <. x , y >. , z >. -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , p ) ps -> ph ) ) )
282 281 3expa 
 |-  ( ( ( x e. No /\ y e. No ) /\ z e. No ) -> ( p = <. <. x , y >. , z >. -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , p ) ps -> ph ) ) )
283 282 rexlimdva 
 |-  ( ( x e. No /\ y e. No ) -> ( E. z e. No p = <. <. x , y >. , z >. -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , p ) ps -> ph ) ) )
284 283 rexlimivv 
 |-  ( E. x e. No E. y e. No E. z e. No p = <. <. x , y >. , z >. -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , p ) ps -> ph ) )
285 28 284 sylbi 
 |-  ( p e. ( ( No X. No ) X. No ) -> ( A. q e. Pred ( S , ( ( No X. No ) X. No ) , p ) ps -> ph ) )
286 285 3 frpoins2g 
 |-  ( ( S Fr ( ( No X. No ) X. No ) /\ S Po ( ( No X. No ) X. No ) /\ S Se ( ( No X. No ) X. No ) ) -> A. p e. ( ( No X. No ) X. No ) ph )
287 19 23 27 286 mp3an 
 |-  A. p e. ( ( No X. No ) X. No ) ph
288 4 ralxp3 
 |-  ( A. p e. ( ( No X. No ) X. No ) ph <-> A. x e. No A. y e. No A. z e. No ch )
289 287 288 mpbi 
 |-  A. x e. No A. y e. No A. z e. No ch
290 12 13 14 rspc3v 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A. x e. No A. y e. No A. z e. No ch -> al ) )
291 289 290 mpi 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> al )