Theorem bnj1110

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1110.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
	bnj1110.7	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj1110.18	No typesetting found for |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
	bnj1110.19	No typesetting found for |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode |-
	bnj1110.26	No typesetting found for |- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |-
Assertion	bnj1110	Could not format assertion : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj1110.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
2		bnj1110.7	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
3		bnj1110.18	Could not format ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
4		bnj1110.19	Could not format ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) : No typesetting found for |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode |-
5		bnj1110.26	Could not format ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) : No typesetting found for |- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |-
6	2	bnj1098	$$⊢\exists j\left(\left(i\ne \varnothing \wedge i\in n\wedge n\in D\right)\to \left(j\in n\wedge i=\mathrm{suc}j\right)\right)$$
7		bnj219	$$⊢i=\mathrm{suc}j\to j\mathrm{E}i$$
8	7	adantl	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\right)\to j\mathrm{E}i$$
9	8	ancli	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\right)\to \left(\left(j\in n\wedge i=\mathrm{suc}j\right)\wedge j\mathrm{E}i\right)$$
10		df-3an	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\wedge j\mathrm{E}i\right)\leftrightarrow \left(\left(j\in n\wedge i=\mathrm{suc}j\right)\wedge j\mathrm{E}i\right)$$
11	9 10	sylibr	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\right)\to \left(j\in n\wedge i=\mathrm{suc}j\wedge j\mathrm{E}i\right)$$
12	6 11	bnj1023	$$⊢\exists j\left(\left(i\ne \varnothing \wedge i\in n\wedge n\in D\right)\to \left(j\in n\wedge i=\mathrm{suc}j\wedge j\mathrm{E}i\right)\right)$$
13	1	bnj1232	$$⊢\chi \to n\in D$$
14	13	3ad2ant3	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to n\in D$$
15	4	bnj1232	Could not format ( ph0 -> i e. n ) : No typesetting found for |- ( ph0 -> i e. n ) with typecode |-
16	14 15	anim12ci	Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( i e. n /\ n e. D ) ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( i e. n /\ n e. D ) ) with typecode |-
17	16	anim2i	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i =/= (/) /\ ( i e. n /\ n e. D ) ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i =/= (/) /\ ( i e. n /\ n e. D ) ) ) with typecode |-
18		3anass	$$⊢\left(i\ne \varnothing \wedge i\in n\wedge n\in D\right)\leftrightarrow \left(i\ne \varnothing \wedge \left(i\in n\wedge n\in D\right)\right)$$
19	17 18	sylibr	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i =/= (/) /\ i e. n /\ n e. D ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i =/= (/) /\ i e. n /\ n e. D ) ) with typecode |-
20	12 19	bnj1101	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) with typecode |-
21		3simpb	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\wedge j\mathrm{E}i\right)\to \left(j\in n\wedge j\mathrm{E}i\right)$$
22	4	bnj1235	Could not format ( ph0 -> si ) : No typesetting found for |- ( ph0 -> si ) with typecode |-
23	22	ad2antll	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> si ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> si ) with typecode |-
24	23 3	sylib	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
25	21 24	syl5	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) -> et' ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) -> et' ) ) with typecode |-
26	25	a2i	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> et' ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> et' ) ) with typecode |-
27		pm3.43	Could not format ( ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) /\ ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) : No typesetting found for |- ( ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) /\ ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) with typecode |-
28	26 27	mpdan	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ j _E i ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) with typecode |-
29	20 28	bnj101	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) with typecode |-
30	4	bnj1247	Could not format ( ph0 -> f e. K ) : No typesetting found for |- ( ph0 -> f e. K ) with typecode |-
31	30	ad2antll	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> f e. K ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> f e. K ) with typecode |-
32		pm3.43i	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> f e. K ) -> ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> f e. K ) -> ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) with typecode |-
33	31 32	ax-mp	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) with typecode |-
34	29 33	bnj101	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) with typecode |-
35		fndm	$$⊢fFnn\to \mathrm{dom}f=n$$
36	1 35	bnj770	$$⊢\chi \to \mathrm{dom}f=n$$
37	36	3ad2ant3	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to \mathrm{dom}f=n$$
38	37	ad2antrl	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> dom f = n ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> dom f = n ) with typecode |-
39	38	eleq2d	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. dom f <-> j e. n ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. dom f <-> j e. n ) ) with typecode |-
40		pm3.43i	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. dom f <-> j e. n ) ) -> ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. dom f <-> j e. n ) ) -> ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) ) with typecode |-
41	39 40	ax-mp	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) with typecode |-
42	34 41	bnj101	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) with typecode |-
43		bnj268	Could not format ( ( ( j e. dom f <-> j e. n ) /\ f e. K /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ f e. K /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) with typecode |-
44		bnj251	Could not format ( ( ( j e. dom f <-> j e. n ) /\ f e. K /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ f e. K /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) with typecode |-
45	43 44	bitr3i	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) <-> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) with typecode |-
46	45	imbi2i	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) <-> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) <-> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) with typecode |-
47	46	exbii	Could not format ( E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) <-> E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) : No typesetting found for |- ( E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) <-> E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( f e. K /\ ( ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) ) ) ) ) with typecode |-
48	42 47	mpbir	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) ) with typecode |-
49		simp1	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\wedge j\mathrm{E}i\right)\to j\in n$$
50	49	bnj706	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> j e. n ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> j e. n ) with typecode |-
51		simp2	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\wedge j\mathrm{E}i\right)\to i=\mathrm{suc}j$$
52	51	bnj706	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> i = suc j ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> i = suc j ) with typecode |-
53		bnj258	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) <-> ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) /\ f e. K ) ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) <-> ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ et' ) /\ f e. K ) ) with typecode |-
54	53	simprbi	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> f e. K ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> f e. K ) with typecode |-
55		bnj642	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( j e. dom f <-> j e. n ) ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( j e. dom f <-> j e. n ) ) with typecode |-
56	50 55	mpbird	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> j e. dom f ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> j e. dom f ) with typecode |-
57		bnj645	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> et' ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> et' ) with typecode |-
58	57 5	sylib	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |-
59	54 56 58	mp2and	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( f ` j ) C_ B ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( f ` j ) C_ B ) with typecode |-
60	50 52 59	3jca	Could not format ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) : No typesetting found for |- ( ( ( j e. dom f <-> j e. n ) /\ ( j e. n /\ i = suc j /\ j _E i ) /\ f e. K /\ et' ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) with typecode |-
61	48 60	bnj1023	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) with typecode |-