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	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1118.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1118.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
	bnj1118.7	$⊢ D = ω ∖ \{\emptyset\}$
	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	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
2		bnj1118.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
3		bnj1118.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
4		bnj1118.7	$⊢ D = ω ∖ \{\emptyset\}$
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	$⊢ χ \to ψ$
13	12	3ad2ant3	$⊢ (θ \land τ \land χ) \to ψ$
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	$⊢ χ \to n \in D$
17	16	3ad2ant3	$⊢ (θ \land τ \land χ) \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 ω$
22	21	anim1i	$⊢ (n \in D \land j \in n) \to (n \in ω \land j \in n)$
23	22	ancomd	$⊢ (n \in D \land j \in n) \to (j \in n \land n \in ω)$
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	$⊢ (j \in n \land n \in ω) \to j \in ω$
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	$⊢ τ \to TrFo (B, A, R)$
32	31	3ad2ant2	$⊢ (θ \land τ \land χ) \to TrFo (B, A, R)$
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	$⊢ (j \in n \land i = suc j \land f (j) \subseteq B) \to f (j) \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	$⊢ (i = suc j \land ψ \land j \in ω \land i \in n) \leftrightarrow ((i = suc j \land ψ) \land (j \in ω \land i \in n))$
37	1	bnj1112	$⊢ ψ \leftrightarrow \forall j ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
38	37	biimpi	$⊢ ψ \to \forall j ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
39	38	19.21bi	$⊢ ψ \to ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
40		eleq1	$⊢ i = suc j \to (i \in n \leftrightarrow suc j \in n)$
41	40	anbi2d	$⊢ i = suc j \to ((j \in ω \land i \in n) \leftrightarrow (j \in ω \land suc j \in n))$
42		fveqeq2	$⊢ i = suc j \to (f (i) = ⋃_{y \in f (j)} pred (y, A, R) \leftrightarrow f (suc j) = ⋃_{y \in f (j)} pred (y, A, R))$
43	41 42	imbi12d	$⊢ i = suc j \to (((j \in ω \land i \in n) \to f (i) = ⋃_{y \in f (j)} pred (y, A, R)) \leftrightarrow ((j \in ω \land suc j \in n) \to f (suc j) = ⋃_{y \in f (j)} pred (y, A, R)))$
44	39 43	imbitrrid	$⊢ i = suc j \to (ψ \to ((j \in ω \land i \in n) \to f (i) = ⋃_{y \in f (j)} pred (y, A, R)))$
45	44	imp31	$⊢ ((i = suc j \land ψ) \land (j \in ω \land i \in n)) \to f (i) = ⋃_{y \in f (j)} pred (y, A, R)$
46	36 45	sylbi	$⊢ (i = suc j \land ψ \land j \in ω \land i \in n) \to f (i) = ⋃_{y \in f (j)} pred (y, A, R)$
47		df-bnj19	$⊢ TrFo (B, A, R) \leftrightarrow \forall y \in B pred (y, A, R) \subseteq B$
48		ssralv	$⊢ f (j) \subseteq B \to (\forall y \in B pred (y, A, R) \subseteq B \to \forall y \in f (j) pred (y, A, R) \subseteq B)$
49	47 48	biimtrid	$⊢ f (j) \subseteq B \to (TrFo (B, A, R) \to \forall y \in f (j) pred (y, A, R) \subseteq B)$
50	49	impcom	$⊢ (TrFo (B, A, R) \land f (j) \subseteq B) \to \forall y \in f (j) pred (y, A, R) \subseteq B$
51		iunss	$⊢ ⋃_{y \in f (j)} pred (y, A, R) \subseteq B \leftrightarrow \forall y \in f (j) pred (y, A, R) \subseteq B$
52	50 51	sylibr	$⊢ (TrFo (B, A, R) \land f (j) \subseteq B) \to ⋃_{y \in f (j)} pred (y, A, R) \subseteq B$
53		sseq1	$⊢ f (i) = ⋃_{y \in f (j)} pred (y, A, R) \to (f (i) \subseteq B \leftrightarrow ⋃_{y \in f (j)} pred (y, A, R) \subseteq B)$
54	53	biimpar	$⊢ (f (i) = ⋃_{y \in f (j)} pred (y, A, R) \land ⋃_{y \in f (j)} pred (y, A, R) \subseteq B) \to f (i) \subseteq B$
55	46 52 54	syl2an	$⊢ ((i = suc j \land ψ \land j \in ω \land i \in n) \land (TrFo (B, A, R) \land f (j) \subseteq B)) \to f (i) \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 \|-

Metamath Proof Explorer

Theorem bnj1118

Proof