Theorem no3inds

Description: Triple induction over surreal numbers. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Hypotheses	no3inds.1	$$⊢a=d\to \left(\phi \leftrightarrow \psi \right)$$
	no3inds.2	$$⊢b=e\to \left(\psi \leftrightarrow \chi \right)$$
	no3inds.3	$$⊢c=f\to \left(\chi \leftrightarrow \theta \right)$$
	no3inds.4	$$⊢a=d\to \left(\tau \leftrightarrow \theta \right)$$
	no3inds.5	$$⊢b=e\to \left(\eta \leftrightarrow \tau \right)$$
	no3inds.6	$$⊢b=e\to \left(\zeta \leftrightarrow \theta \right)$$
	no3inds.7	$$⊢c=f\to \left(\sigma \leftrightarrow \tau \right)$$
	no3inds.8	$$⊢a=X\to \left(\phi \leftrightarrow \rho \right)$$
	no3inds.9	$$⊢b=Y\to \left(\rho \leftrightarrow \mu \right)$$
	no3inds.10	$$⊢c=Z\to \left(\mu \leftrightarrow \lambda \right)$$
	no3inds.i	No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) /\ ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) /\ A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) et ) -> ph ) ) with typecode |-
Assertion	no3inds	$$⊢\left(X\in \mathrm{No}\wedge Y\in \mathrm{No}\wedge Z\in \mathrm{No}\right)\to \lambda$$

Proof

Step	Hyp	Ref	Expression
1		no3inds.1	$$⊢a=d\to \left(\phi \leftrightarrow \psi \right)$$
2		no3inds.2	$$⊢b=e\to \left(\psi \leftrightarrow \chi \right)$$
3		no3inds.3	$$⊢c=f\to \left(\chi \leftrightarrow \theta \right)$$
4		no3inds.4	$$⊢a=d\to \left(\tau \leftrightarrow \theta \right)$$
5		no3inds.5	$$⊢b=e\to \left(\eta \leftrightarrow \tau \right)$$
6		no3inds.6	$$⊢b=e\to \left(\zeta \leftrightarrow \theta \right)$$
7		no3inds.7	$$⊢c=f\to \left(\sigma \leftrightarrow \tau \right)$$
8		no3inds.8	$$⊢a=X\to \left(\phi \leftrightarrow \rho \right)$$
9		no3inds.9	$$⊢b=Y\to \left(\rho \leftrightarrow \mu \right)$$
10		no3inds.10	$$⊢c=Z\to \left(\mu \leftrightarrow \lambda \right)$$
11		no3inds.i	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) /\ ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) /\ A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) et ) -> ph ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) /\ ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) /\ A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) et ) -> ph ) ) with typecode |-
12		eqid	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
13	12	lrrecfr	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Fr No with typecode |-
14	12	lrrecpo	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Po No with typecode |-
15	12	lrrecse	Could not format { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No : No typesetting found for |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } Se No with typecode |-
16	12	lrrecpred	Could not format ( a e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) = ( ( _Left ` a ) u. ( _Right ` a ) ) ) : No typesetting found for |- ( a e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) = ( ( _Left ` a ) u. ( _Right ` a ) ) ) with typecode |-
17	16	3ad2ant1	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) = ( ( _Left ` a ) u. ( _Right ` a ) ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) = ( ( _Left ` a ) u. ( _Right ` a ) ) ) with typecode |-
18	12	lrrecpred	Could not format ( b e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) = ( ( _Left ` b ) u. ( _Right ` b ) ) ) : No typesetting found for |- ( b e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) = ( ( _Left ` b ) u. ( _Right ` b ) ) ) with typecode |-
19	18	3ad2ant2	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) = ( ( _Left ` b ) u. ( _Right ` b ) ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) = ( ( _Left ` b ) u. ( _Right ` b ) ) ) with typecode |-
20	12	lrrecpred	Could not format ( c e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) = ( ( _Left ` c ) u. ( _Right ` c ) ) ) : No typesetting found for |- ( c e. No -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) = ( ( _Left ` c ) u. ( _Right ` c ) ) ) with typecode |-
21	20	3ad2ant3	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) = ( ( _Left ` c ) u. ( _Right ` c ) ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) = ( ( _Left ` c ) u. ( _Right ` c ) ) ) with typecode |-
22	21	raleqdv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th ) ) with typecode |-
23	19 22	raleqbidv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th ) ) with typecode |-
24	17 23	raleqbidv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th ) ) with typecode |-
25	19	raleqdv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch ) ) with typecode |-
26	17 25	raleqbidv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch ) ) with typecode |-
27	21	raleqdv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) ) with typecode |-
28	17 27	raleqbidv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) ) with typecode |-
29	24 26 28	3anbi123d	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze ) <-> ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze ) <-> ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) ) ) with typecode |-
30	17	raleqdv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps <-> A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps ) ) with typecode |-
31	21	raleqdv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta ) ) with typecode |-
32	19 31	raleqbidv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta ) ) with typecode |-
33	19	raleqdv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si <-> A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) ) with typecode |-
34	30 32 33	3anbi123d	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si ) <-> ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si ) <-> ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) ) ) with typecode |-
35	21	raleqdv	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) et <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) et ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) et <-> A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) et ) ) with typecode |-
36	29 34 35	3anbi123d	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze ) /\ ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si ) /\ A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) et ) <-> ( ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) /\ ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) /\ A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) et ) ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze ) /\ ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si ) /\ A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) et ) <-> ( ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) th /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) ch /\ A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ze ) /\ ( A. d e. ( ( _Left ` a ) u. ( _Right ` a ) ) ps /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) ta /\ A. e e. ( ( _Left ` b ) u. ( _Right ` b ) ) si ) /\ A. f e. ( ( _Left ` c ) u. ( _Right ` c ) ) et ) ) ) with typecode |-
37	36 11	sylbid	Could not format ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze ) /\ ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si ) /\ A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) et ) -> ph ) ) : No typesetting found for |- ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ze ) /\ ( A. d e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , b ) si ) /\ A. f e. Pred ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , c ) et ) -> ph ) ) with typecode |-
38	13 14 15 13 14 15 13 14 15 1 2 3 4 5 6 7 8 9 10 37	xpord3ind	$$⊢\left(X\in \mathrm{No}\wedge Y\in \mathrm{No}\wedge Z\in \mathrm{No}\right)\to \lambda$$