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	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1110.7	$⊢ D = ω ∖ \{\emptyset\}$
	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	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
2		bnj1110.7	$⊢ D = ω ∖ \{\emptyset\}$
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 ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in n \land i = suc j))$
7		bnj219	$⊢ i = suc j \to j E i$
8	7	adantl	$⊢ (j \in n \land i = suc j) \to j E i$
9	8	ancli	$⊢ (j \in n \land i = suc j) \to ((j \in n \land i = suc j) \land j E i)$
10		df-3an	$⊢ (j \in n \land i = suc j \land j E i) \leftrightarrow ((j \in n \land i = suc j) \land j E i)$
11	9 10	sylibr	$⊢ (j \in n \land i = suc j) \to (j \in n \land i = suc j \land j E i)$
12	6 11	bnj1023	$⊢ \exists j ((i \neq \emptyset \land i \in n \land n \in D) \to (j \in n \land i = suc j \land j E i))$
13	1	bnj1232	$⊢ χ \to n \in D$
14	13	3ad2ant3	$⊢ (θ \land τ \land χ) \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	$⊢ (i \neq \emptyset \land i \in n \land n \in D) \leftrightarrow (i \neq \emptyset \land (i \in n \land n \in D))$
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	$⊢ (j \in n \land i = suc j \land j E i) \to (j \in n \land j E i)$
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	$⊢ f Fn n \to dom f = n$
36	1 35	bnj770	$⊢ χ \to dom f = n$
37	36	3ad2ant3	$⊢ (θ \land τ \land χ) \to 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	$⊢ (j \in n \land i = suc j \land j E i) \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	$⊢ (j \in n \land i = suc j \land j E i) \to i = 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 \|-

Metamath Proof Explorer

Theorem bnj1110

Proof