bnj571

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	bnj571.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj571.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
	bnj571.17	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj571.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
	bnj571.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj571.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
	bnj571.22	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
	bnj571.23	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
	bnj571.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
	bnj571.25	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
	bnj571.26	$⊢ G = f \cup \{⟨m, C⟩\}$
	bnj571.29	No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
	bnj571.30	No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
	bnj571.38	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
	bnj571.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
	bnj571.40	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
	bnj571.33	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 \|-
Assertion	bnj571	Could not format assertion : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj571.3	$⊢ D = ω ∖ \{\emptyset\}$
2		bnj571.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
3		bnj571.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
4		bnj571.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
5		bnj571.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
6		bnj571.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
7		bnj571.22	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
8		bnj571.23	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
9		bnj571.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
10		bnj571.25	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
11		bnj571.26	$⊢ G = f \cup \{⟨m, C⟩\}$
12		bnj571.29	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
13		bnj571.30	Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
14		bnj571.38	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
15		bnj571.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
16		bnj571.40	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
17		bnj571.33	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 \|-
18		nfv	$⊢ Ⅎ i R FrSe A$
19		nfv	$⊢ Ⅎ i f Fn m$
20		nfv	Could not format F/ i ph' : No typesetting found for \|- F/ i ph' with typecode \|-
21		nfra1	$⊢ Ⅎ i \forall i \in ω (suc i \in m \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
22	13 21	nfxfr	Could not format F/ i ps' : No typesetting found for \|- F/ i ps' with typecode \|-
23	19 20 22	nf3an	Could not format F/ i ( f Fn m /\ ph' /\ ps' ) : No typesetting found for \|- F/ i ( f Fn m /\ ph' /\ ps' ) with typecode \|-
24	3 23	nfxfr	$⊢ Ⅎ i τ$
25		nfv	$⊢ Ⅎ i η$
26	18 24 25	nf3an	$⊢ Ⅎ i (R FrSe A \land τ \land η)$
27		df-bnj17	$⊢ (R FrSe A \land τ \land η \land ζ) \leftrightarrow ((R FrSe A \land τ \land η) \land ζ)$
28		3anass	$⊢ ((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n) \land m = suc i) \leftrightarrow ((R FrSe A \land τ \land η) \land ((i \in ω \land suc i \in n) \land m = suc i))$
29		3anrot	$⊢ (m = suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \leftrightarrow ((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n) \land m = suc i)$
30		df-3an	$⊢ (i \in ω \land suc i \in n \land m = suc i) \leftrightarrow ((i \in ω \land suc i \in n) \land m = suc i)$
31	6 30	bitri	$⊢ ζ \leftrightarrow ((i \in ω \land suc i \in n) \land m = suc i)$
32	31	anbi2i	$⊢ ((R FrSe A \land τ \land η) \land ζ) \leftrightarrow ((R FrSe A \land τ \land η) \land ((i \in ω \land suc i \in n) \land m = suc i))$
33	28 29 32	3bitr4ri	$⊢ ((R FrSe A \land τ \land η) \land ζ) \leftrightarrow (m = suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n))$
34	27 33	bitri	$⊢ (R FrSe A \land τ \land η \land ζ) \leftrightarrow (m = suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n))$
35	1 2 3 4 5 6 7 8 9 10 11 12 13 14	bnj558	$⊢ (R FrSe A \land τ \land η \land ζ) \to G (suc i) = K$
36	34 35	sylbir	$⊢ (m = suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \to G (suc i) = K$
37	36	3expib	$⊢ m = suc i \to (((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \to G (suc i) = K)$
38		df-bnj17	$⊢ (R FrSe A \land τ \land η \land ρ) \leftrightarrow ((R FrSe A \land τ \land η) \land ρ)$
39		3anass	$⊢ ((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n) \land m \neq suc i) \leftrightarrow ((R FrSe A \land τ \land η) \land ((i \in ω \land suc i \in n) \land m \neq suc i))$
40		3anrot	$⊢ (m \neq suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \leftrightarrow ((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n) \land m \neq suc i)$
41		df-3an	$⊢ (i \in ω \land suc i \in n \land m \neq suc i) \leftrightarrow ((i \in ω \land suc i \in n) \land m \neq suc i)$
42	15 41	bitri	$⊢ ρ \leftrightarrow ((i \in ω \land suc i \in n) \land m \neq suc i)$
43	42	anbi2i	$⊢ ((R FrSe A \land τ \land η) \land ρ) \leftrightarrow ((R FrSe A \land τ \land η) \land ((i \in ω \land suc i \in n) \land m \neq suc i))$
44	39 40 43	3bitr4ri	$⊢ ((R FrSe A \land τ \land η) \land ρ) \leftrightarrow (m \neq suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n))$
45	38 44	bitri	$⊢ (R FrSe A \land τ \land η \land ρ) \leftrightarrow (m \neq suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n))$
46	1 3 5 15 9 2 16 13	bnj570	$⊢ (R FrSe A \land τ \land η \land ρ) \to G (suc i) = K$
47	45 46	sylbir	$⊢ (m \neq suc i \land (R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \to G (suc i) = K$
48	47	3expib	$⊢ m \neq suc i \to (((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \to G (suc i) = K)$
49	37 48	pm2.61ine	$⊢ ((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \to G (suc i) = K$
50	49 9	eqtrdi	$⊢ ((R FrSe A \land τ \land η) \land (i \in ω \land suc i \in n)) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
51	50	exp32	$⊢ (R FrSe A \land τ \land η) \to (i \in ω \to (suc i \in n \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)))$
52	26 51	alrimi	$⊢ (R FrSe A \land τ \land η) \to \forall i (i \in ω \to (suc i \in n \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)))$
53	17	bnj946	Could not format ( ps" <-> A. i ( 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 ( i e. _om -> ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) ) with typecode \|-
54	52 53	sylibr	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-

Metamath Proof Explorer

Theorem bnj571

Proof