bnj594

Description: Technical lemma for bnj852 . 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	bnj594.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj594.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj594.3	$⊢ χ \leftrightarrow (f Fn n \land φ \land ψ)$
	bnj594.7	$⊢ D = ω ∖ \{\emptyset\}$
	bnj594.9	No typesetting found for \|- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
	bnj594.10	No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode \|-
	bnj594.11	No typesetting found for \|- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode \|-
	bnj594.15	No typesetting found for \|- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
	bnj594.16	No typesetting found for \|- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode \|-
	bnj594.17	$⊢ τ \leftrightarrow \forall k \in n (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ)$
Assertion	bnj594	$⊢ (j \in n \land τ) \to θ$

Proof

Step	Hyp	Ref	Expression
1		bnj594.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj594.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj594.3	$⊢ χ \leftrightarrow (f Fn n \land φ \land ψ)$
4		bnj594.7	$⊢ D = ω ∖ \{\emptyset\}$
5		bnj594.9	Could not format ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
6		bnj594.10	Could not format ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode \|-
7		bnj594.11	Could not format ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode \|-
8		bnj594.15	Could not format ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
9		bnj594.16	Could not format ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) : No typesetting found for \|- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode \|-
10		bnj594.17	$⊢ τ \leftrightarrow \forall k \in n (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ)$
11	3	simp2bi	$⊢ χ \to φ$
12	11 1	sylib	$⊢ χ \to f (\emptyset) = pred (x, A, R)$
13	7	simp2bi	Could not format ( ch' -> ph' ) : No typesetting found for \|- ( ch' -> ph' ) with typecode \|-
14	13 5	sylib	Could not format ( ch' -> ( g ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ch' -> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
15		eqtr3	$⊢ (f (\emptyset) = pred (x, A, R) \land g (\emptyset) = pred (x, A, R)) \to f (\emptyset) = g (\emptyset)$
16	12 14 15	syl2an	Could not format ( ( ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) : No typesetting found for \|- ( ( ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) with typecode \|-
17	16	3adant1	Could not format ( ( n e. D /\ ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) : No typesetting found for \|- ( ( n e. D /\ ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) with typecode \|-
18		fveq2	$⊢ j = \emptyset \to f (j) = f (\emptyset)$
19		fveq2	$⊢ j = \emptyset \to g (j) = g (\emptyset)$
20	18 19	eqeq12d	$⊢ j = \emptyset \to (f (j) = g (j) \leftrightarrow f (\emptyset) = g (\emptyset))$
21	17 20	imbitrrid	Could not format ( j = (/) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( j = (/) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
22	21 8	sylibr	$⊢ j = \emptyset \to θ$
23	22	a1d	$⊢ j = \emptyset \to ((j \in n \land τ) \to θ)$
24		bnj253	Could not format ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) ) : No typesetting found for \|- ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) ) with typecode \|-
25		bnj252	Could not format ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for \|- ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode \|-
26		anidm	$⊢ (n \in D \land n \in D) \leftrightarrow n \in D$
27	26	3anbi1i	Could not format ( ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) <-> ( n e. D /\ ch /\ ch' ) ) : No typesetting found for \|- ( ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) <-> ( n e. D /\ ch /\ ch' ) ) with typecode \|-
28	24 25 27	3bitr3i	Could not format ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) <-> ( n e. D /\ ch /\ ch' ) ) : No typesetting found for \|- ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) <-> ( n e. D /\ ch /\ ch' ) ) with typecode \|-
29		df-bnj17	$⊢ (j \neq \emptyset \land j \in n \land n \in D \land τ) \leftrightarrow ((j \neq \emptyset \land j \in n \land n \in D) \land τ)$
30	10	bnj1095	$⊢ τ \to \forall k τ$
31	30	bnj1352	$⊢ ((j \neq \emptyset \land j \in n \land n \in D) \land τ) \to \forall k ((j \neq \emptyset \land j \in n \land n \in D) \land τ)$
32	29 31	hbxfrbi	$⊢ (j \neq \emptyset \land j \in n \land n \in D \land τ) \to \forall k (j \neq \emptyset \land j \in n \land n \in D \land τ)$
33		bnj170	$⊢ (j \neq \emptyset \land j \in n \land n \in D) \leftrightarrow ((j \in n \land n \in D) \land j \neq \emptyset)$
34	4	bnj923	$⊢ n \in D \to n \in ω$
35		elnn	$⊢ (j \in n \land n \in ω) \to j \in ω$
36	34 35	sylan2	$⊢ (j \in n \land n \in D) \to j \in ω$
37	36	anim1i	$⊢ ((j \in n \land n \in D) \land j \neq \emptyset) \to (j \in ω \land j \neq \emptyset)$
38	33 37	sylbi	$⊢ (j \neq \emptyset \land j \in n \land n \in D) \to (j \in ω \land j \neq \emptyset)$
39		nnsuc	$⊢ (j \in ω \land j \neq \emptyset) \to \exists k \in ω j = suc k$
40		rexex	$⊢ \exists k \in ω j = suc k \to \exists k j = suc k$
41	38 39 40	3syl	$⊢ (j \neq \emptyset \land j \in n \land n \in D) \to \exists k j = suc k$
42	41	bnj721	$⊢ (j \neq \emptyset \land j \in n \land n \in D \land τ) \to \exists k j = suc k$
43	32 42	bnj596	$⊢ (j \neq \emptyset \land j \in n \land n \in D \land τ) \to \exists k ((j \neq \emptyset \land j \in n \land n \in D \land τ) \land j = suc k)$
44		bnj667	$⊢ (j \neq \emptyset \land j \in n \land n \in D \land τ) \to (j \in n \land n \in D \land τ)$
45	44	anim1i	$⊢ ((j \neq \emptyset \land j \in n \land n \in D \land τ) \land j = suc k) \to ((j \in n \land n \in D \land τ) \land j = suc k)$
46		bnj258	$⊢ (j \in n \land n \in D \land j = suc k \land τ) \leftrightarrow ((j \in n \land n \in D \land τ) \land j = suc k)$
47	45 46	sylibr	$⊢ ((j \neq \emptyset \land j \in n \land n \in D \land τ) \land j = suc k) \to (j \in n \land n \in D \land j = suc k \land τ)$
48		df-bnj17	$⊢ (j \in n \land n \in D \land j = suc k \land τ) \leftrightarrow ((j \in n \land n \in D \land j = suc k) \land τ)$
49		bnj219	$⊢ j = suc k \to k E j$
50	49	3ad2ant3	$⊢ (j \in n \land n \in D \land j = suc k) \to k E j$
51	50	adantr	$⊢ ((j \in n \land n \in D \land j = suc k) \land τ) \to k E j$
52		vex	$⊢ k \in V$
53	52	bnj216	$⊢ j = suc k \to k \in j$
54		df-3an	$⊢ (k \in j \land j \in n \land n \in D) \leftrightarrow ((k \in j \land j \in n) \land n \in D)$
55		3anrot	$⊢ (k \in j \land j \in n \land n \in D) \leftrightarrow (j \in n \land n \in D \land k \in j)$
56		ancom	$⊢ ((k \in j \land j \in n) \land n \in D) \leftrightarrow (n \in D \land (k \in j \land j \in n))$
57	54 55 56	3bitr3i	$⊢ (j \in n \land n \in D \land k \in j) \leftrightarrow (n \in D \land (k \in j \land j \in n))$
58		eldifi	$⊢ n \in (ω ∖ \{\emptyset\}) \to n \in ω$
59	58 4	eleq2s	$⊢ n \in D \to n \in ω$
60		nnord	$⊢ n \in ω \to Ord n$
61		ordtr1	$⊢ Ord n \to ((k \in j \land j \in n) \to k \in n)$
62	59 60 61	3syl	$⊢ n \in D \to ((k \in j \land j \in n) \to k \in n)$
63	62	imp	$⊢ (n \in D \land (k \in j \land j \in n)) \to k \in n$
64	57 63	sylbi	$⊢ (j \in n \land n \in D \land k \in j) \to k \in n$
65	53 64	syl3an3	$⊢ (j \in n \land n \in D \land j = suc k) \to k \in n$
66		rsp	$⊢ \forall k \in n (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ) \to (k \in n \to (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ))$
67	10 66	sylbi	$⊢ τ \to (k \in n \to (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ))$
68	65 67	mpan9	$⊢ ((j \in n \land n \in D \land j = suc k) \land τ) \to (k E j \to \underset{˙}{[} k / j \underset{˙}{]} θ)$
69	51 68	mpd	$⊢ ((j \in n \land n \in D \land j = suc k) \land τ) \to \underset{˙}{[} k / j \underset{˙}{]} θ$
70	48 69	sylbi	$⊢ (j \in n \land n \in D \land j = suc k \land τ) \to \underset{˙}{[} k / j \underset{˙}{]} θ$
71	70	anim1i	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode \|-
72		bnj252	Could not format ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for \|- ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode \|-
73	71 72	sylibr	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) ) with typecode \|-
74		bnj446	Could not format ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) ) : No typesetting found for \|- ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) ) with typecode \|-
75		pm3.35	Could not format ( ( ( n e. D /\ ch /\ ch' ) /\ ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) -> ( f ` k ) = ( g ` k ) ) : No typesetting found for \|- ( ( ( n e. D /\ ch /\ ch' ) /\ ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) -> ( f ` k ) = ( g ` k ) ) with typecode \|-
76	9 75	sylan2b	Could not format ( ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) -> ( f ` k ) = ( g ` k ) ) : No typesetting found for \|- ( ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) -> ( f ` k ) = ( g ` k ) ) with typecode \|-
77	74 76	sylbi	Could not format ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) : No typesetting found for \|- ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) with typecode \|-
78		iuneq1	$⊢ f (k) = g (k) \to ⋃_{y \in f (k)} pred (y, A, R) = ⋃_{y \in g (k)} pred (y, A, R)$
79	73 77 78	3syl	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> U_ y e. ( f ` k ) _pred ( y , A , R ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> U_ y e. ( f ` k ) _pred ( y , A , R ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode \|-
80		bnj658	$⊢ (j \in n \land n \in D \land j = suc k \land τ) \to (j \in n \land n \in D \land j = suc k)$
81	3	simp3bi	$⊢ χ \to ψ$
82	7	simp3bi	Could not format ( ch' -> ps' ) : No typesetting found for \|- ( ch' -> ps' ) with typecode \|-
83	81 82	bnj240	Could not format ( ( n e. D /\ ch /\ ch' ) -> ( ps /\ ps' ) ) : No typesetting found for \|- ( ( n e. D /\ ch /\ ch' ) -> ( ps /\ ps' ) ) with typecode \|-
84	80 83	anim12i	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) ) with typecode \|-
85		simpl	Could not format ( ( ps /\ ps' ) -> ps ) : No typesetting found for \|- ( ( ps /\ ps' ) -> ps ) with typecode \|-
86	85	anim2i	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps ) ) with typecode \|-
87		simp3	$⊢ (j \in n \land n \in D \land j = suc k) \to j = suc k$
88	87	anim1i	$⊢ ((j \in n \land n \in D \land j = suc k) \land ψ) \to (j = suc k \land ψ)$
89		simpl1	$⊢ ((j \in n \land n \in D \land j = suc k) \land (j = suc k \land ψ)) \to j \in n$
90		df-3an	$⊢ (j \in n \land n \in D \land j = suc k) \leftrightarrow ((j \in n \land n \in D) \land j = suc k)$
91	90	biancomi	$⊢ (j \in n \land n \in D \land j = suc k) \leftrightarrow (j = suc k \land (j \in n \land n \in D))$
92		elnn	$⊢ (k \in j \land j \in ω) \to k \in ω$
93	53 36 92	syl2an	$⊢ (j = suc k \land (j \in n \land n \in D)) \to k \in ω$
94	91 93	sylbi	$⊢ (j \in n \land n \in D \land j = suc k) \to k \in ω$
95	2	bnj589	$⊢ ψ \leftrightarrow \forall k \in ω (suc k \in n \to f (suc k) = ⋃_{y \in f (k)} pred (y, A, R))$
96	95	bnj590	$⊢ (j = suc k \land ψ) \to (k \in ω \to (j \in n \to f (j) = ⋃_{y \in f (k)} pred (y, A, R)))$
97	94 96	mpan9	$⊢ ((j \in n \land n \in D \land j = suc k) \land (j = suc k \land ψ)) \to (j \in n \to f (j) = ⋃_{y \in f (k)} pred (y, A, R))$
98	89 97	mpd	$⊢ ((j \in n \land n \in D \land j = suc k) \land (j = suc k \land ψ)) \to f (j) = ⋃_{y \in f (k)} pred (y, A, R)$
99	88 98	syldan	$⊢ ((j \in n \land n \in D \land j = suc k) \land ψ) \to f (j) = ⋃_{y \in f (k)} pred (y, A, R)$
100	84 86 99	3syl	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) ) with typecode \|-
101		simpr	Could not format ( ( ps /\ ps' ) -> ps' ) : No typesetting found for \|- ( ( ps /\ ps' ) -> ps' ) with typecode \|-
102	101	anim2i	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) ) with typecode \|-
103	87	anim1i	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( j = suc k /\ ps' ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( j = suc k /\ ps' ) ) with typecode \|-
104		simpl1	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> j e. n ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> j e. n ) with typecode \|-
105	6	bnj589	Could not format ( ps' <-> A. k e. _om ( suc k e. n -> ( g ` suc k ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. k e. _om ( suc k e. n -> ( g ` suc k ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) with typecode \|-
106	105	bnj590	Could not format ( ( j = suc k /\ ps' ) -> ( k e. _om -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) ) : No typesetting found for \|- ( ( j = suc k /\ ps' ) -> ( k e. _om -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) ) with typecode \|-
107	94 106	mpan9	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) with typecode \|-
108	104 107	mpd	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode \|-
109	103 108	syldan	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode \|-
110	84 102 109	3syl	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode \|-
111	79 100 110	3eqtr4d	Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) : No typesetting found for \|- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) with typecode \|-
112	111	ex	Could not format ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
113	47 112	syl	Could not format ( ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
114	43 113	bnj593	Could not format ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
115		bnj258	$⊢ (j \neq \emptyset \land j \in n \land n \in D \land τ) \leftrightarrow ((j \neq \emptyset \land j \in n \land τ) \land n \in D)$
116		19.9v	Could not format ( E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
117	114 115 116	3imtr3i	Could not format ( ( ( j =/= (/) /\ j e. n /\ ta ) /\ n e. D ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( ( ( j =/= (/) /\ j e. n /\ ta ) /\ n e. D ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
118	117	expimpd	Could not format ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
119	28 118	biimtrrid	Could not format ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for \|- ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode \|-
120	119 8	sylibr	$⊢ (j \neq \emptyset \land j \in n \land τ) \to θ$
121	120	3expib	$⊢ j \neq \emptyset \to ((j \in n \land τ) \to θ)$
122	23 121	pm2.61ine	$⊢ (j \in n \land τ) \to θ$

Metamath Proof Explorer

Theorem bnj594

Proof