Theorem bnj1118

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	bnj1118.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
	bnj1118.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
	bnj1118.5	$$⊢\tau \leftrightarrow \left(B\in \mathrm{V}\wedge TrFo\left(B,A,R\right)\wedge pred\left(X,A,R\right)\subseteq B\right)$$
	bnj1118.7	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj1118.18	No typesetting found for |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
	bnj1118.19	No typesetting found for |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode |-
	bnj1118.26	No typesetting found for |- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |-
Assertion	bnj1118	Could not format assertion : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj1118.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
2		bnj1118.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
3		bnj1118.5	$$⊢\tau \leftrightarrow \left(B\in \mathrm{V}\wedge TrFo\left(B,A,R\right)\wedge pred\left(X,A,R\right)\subseteq B\right)$$
4		bnj1118.7	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
5		bnj1118.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 |-
6		bnj1118.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 |-
7		bnj1118.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 |-
8	2 4 5 6 7	bnj1110	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 |-
9		ancl	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) ) with typecode |-
10	8 9	bnj101	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( 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 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) with typecode |-
11		simpr2	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i = suc j ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i = suc j ) with typecode |-
12	2	bnj1254	$$⊢\chi \to \psi$$
13	12	3ad2ant3	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to \psi$$
14	13	ad2antrl	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ps ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ps ) with typecode |-
15	14	adantr	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ps ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ps ) with typecode |-
16	2	bnj1232	$$⊢\chi \to n\in D$$
17	16	3ad2ant3	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to n\in D$$
18	17	ad2antrl	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> n e. D ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> n e. D ) with typecode |-
19	18	adantr	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> n e. D ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> n e. D ) with typecode |-
20		simpr1	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. n ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. n ) with typecode |-
21	4	bnj923	$$⊢n\in D\to n\in \mathrm{\omega }$$
22	21	anim1i	$$⊢\left(n\in D\wedge j\in n\right)\to \left(n\in \mathrm{\omega }\wedge j\in n\right)$$
23	22	ancomd	$$⊢\left(n\in D\wedge j\in n\right)\to \left(j\in n\wedge n\in \mathrm{\omega }\right)$$
24	19 20 23	syl2anc	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( j e. n /\ n e. _om ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( j e. n /\ n e. _om ) ) with typecode |-
25		elnn	$$⊢\left(j\in n\wedge n\in \mathrm{\omega }\right)\to j\in \mathrm{\omega }$$
26	24 25	syl	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. _om ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. _om ) with typecode |-
27	6	bnj1232	Could not format ( ph0 -> i e. n ) : No typesetting found for |- ( ph0 -> i e. n ) with typecode |-
28	27	adantl	Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> i e. n ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> i e. n ) with typecode |-
29	28	ad2antlr	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i e. n ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i e. n ) with typecode |-
30	11 15 26 29	bnj951	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( i = suc j /\ ps /\ j e. _om /\ i e. n ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( i = suc j /\ ps /\ j e. _om /\ i e. n ) ) with typecode |-
31	3	simp2bi	$$⊢\tau \to TrFo\left(B,A,R\right)$$
32	31	3ad2ant2	$$⊢\left(\theta \wedge \tau \wedge \chi \right)\to TrFo\left(B,A,R\right)$$
33	32	ad2antrl	Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> _TrFo ( B , A , R ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> _TrFo ( B , A , R ) ) with typecode |-
34		simp3	$$⊢\left(j\in n\wedge i=\mathrm{suc}j\wedge f\left(j\right)\subseteq B\right)\to f\left(j\right)\subseteq B$$
35	33 34	anim12i	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( _TrFo ( B , A , R ) /\ ( f ` j ) C_ B ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( _TrFo ( B , A , R ) /\ ( f ` j ) C_ B ) ) with typecode |-
36		bnj256	$$⊢\left(i=\mathrm{suc}j\wedge \psi \wedge j\in \mathrm{\omega }\wedge i\in n\right)\leftrightarrow \left(\left(i=\mathrm{suc}j\wedge \psi \right)\wedge \left(j\in \mathrm{\omega }\wedge i\in n\right)\right)$$
37	1	bnj1112	$$⊢\psi \leftrightarrow \forall j\left(\left(j\in \mathrm{\omega }\wedge \mathrm{suc}j\in n\right)\to f\left(\mathrm{suc}j\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\right)$$
38	37	biimpi	$$⊢\psi \to \forall j\left(\left(j\in \mathrm{\omega }\wedge \mathrm{suc}j\in n\right)\to f\left(\mathrm{suc}j\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\right)$$
39	38	19.21bi	$$⊢\psi \to \left(\left(j\in \mathrm{\omega }\wedge \mathrm{suc}j\in n\right)\to f\left(\mathrm{suc}j\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\right)$$
40		eleq1	$$⊢i=\mathrm{suc}j\to \left(i\in n\leftrightarrow \mathrm{suc}j\in n\right)$$
41	40	anbi2d	$$⊢i=\mathrm{suc}j\to \left(\left(j\in \mathrm{\omega }\wedge i\in n\right)\leftrightarrow \left(j\in \mathrm{\omega }\wedge \mathrm{suc}j\in n\right)\right)$$
42		fveqeq2	$$⊢i=\mathrm{suc}j\to \left(f\left(i\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\leftrightarrow f\left(\mathrm{suc}j\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\right)$$
43	41 42	imbi12d	$$⊢i=\mathrm{suc}j\to \left(\left(\left(j\in \mathrm{\omega }\wedge i\in n\right)\to f\left(i\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\right)\leftrightarrow \left(\left(j\in \mathrm{\omega }\wedge \mathrm{suc}j\in n\right)\to f\left(\mathrm{suc}j\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\right)\right)$$
44	39 43	syl5ibr	$$⊢i=\mathrm{suc}j\to \left(\psi \to \left(\left(j\in \mathrm{\omega }\wedge i\in n\right)\to f\left(i\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\right)\right)$$
45	44	imp31	$$⊢\left(\left(i=\mathrm{suc}j\wedge \psi \right)\wedge \left(j\in \mathrm{\omega }\wedge i\in n\right)\right)\to f\left(i\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)$$
46	36 45	sylbi	$$⊢\left(i=\mathrm{suc}j\wedge \psi \wedge j\in \mathrm{\omega }\wedge i\in n\right)\to f\left(i\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)$$
47		df-bnj19	$$⊢TrFo\left(B,A,R\right)\leftrightarrow \forall y\in Bpred\left(y,A,R\right)\subseteq B$$
48		ssralv	$$⊢f\left(j\right)\subseteq B\to \left(\forall y\in Bpred\left(y,A,R\right)\subseteq B\to \forall y\in f\left(j\right)pred\left(y,A,R\right)\subseteq B\right)$$
49	47 48	syl5bi	$$⊢f\left(j\right)\subseteq B\to \left(TrFo\left(B,A,R\right)\to \forall y\in f\left(j\right)pred\left(y,A,R\right)\subseteq B\right)$$
50	49	impcom	$$⊢\left(TrFo\left(B,A,R\right)\wedge f\left(j\right)\subseteq B\right)\to \forall y\in f\left(j\right)pred\left(y,A,R\right)\subseteq B$$
51		iunss	$$⊢\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\subseteq B\leftrightarrow \forall y\in f\left(j\right)pred\left(y,A,R\right)\subseteq B$$
52	50 51	sylibr	$$⊢\left(TrFo\left(B,A,R\right)\wedge f\left(j\right)\subseteq B\right)\to \bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\subseteq B$$
53		sseq1	$$⊢f\left(i\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\to \left(f\left(i\right)\subseteq B\leftrightarrow \bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\subseteq B\right)$$
54	53	biimpar	$$⊢\left(f\left(i\right)=\bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\wedge \bigcup _{y\in f\left(j\right)}pred\left(y,A,R\right)\subseteq B\right)\to f\left(i\right)\subseteq B$$
55	46 52 54	syl2an	$$⊢\left(\left(i=\mathrm{suc}j\wedge \psi \wedge j\in \mathrm{\omega }\wedge i\in n\right)\wedge \left(TrFo\left(B,A,R\right)\wedge f\left(j\right)\subseteq B\right)\right)\to f\left(i\right)\subseteq B$$
56	30 35 55	syl2anc	Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( f ` i ) C_ B ) with typecode |-
57	10 56	bnj1023	Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-