bnj570

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	bnj570.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj570.17	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj570.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj570.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
	bnj570.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
	bnj570.26	$⊢ G = f \cup \{⟨m, C⟩\}$
	bnj570.40	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
	bnj570.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 \|-
Assertion	bnj570	$⊢ (R FrSe A \land τ \land η \land ρ) \to G (suc i) = K$

Proof

Step	Hyp	Ref	Expression
1		bnj570.3	$⊢ D = ω ∖ \{\emptyset\}$
2		bnj570.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
3		bnj570.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
4		bnj570.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
5		bnj570.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
6		bnj570.26	$⊢ G = f \cup \{⟨m, C⟩\}$
7		bnj570.40	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
8		bnj570.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 \|-
9		bnj251	$⊢ (R FrSe A \land τ \land η \land ρ) \leftrightarrow (R FrSe A \land (τ \land (η \land ρ)))$
10	2	simp3bi	Could not format ( ta -> ps' ) : No typesetting found for \|- ( ta -> ps' ) with typecode \|-
11	4	simp1bi	$⊢ ρ \to i \in ω$
12	11	adantl	$⊢ (η \land ρ) \to i \in ω$
13	3 4	bnj563	$⊢ (η \land ρ) \to suc i \in m$
14	12 13	jca	$⊢ (η \land ρ) \to (i \in ω \land suc i \in m)$
15	8	bnj946	Could not format ( ps' <-> A. i ( 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 ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) with typecode \|-
16		sp	$⊢ \forall i (i \in ω \to (suc i \in m \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))) \to (i \in ω \to (suc i \in m \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
17	15 16	sylbi	Could not format ( ps' -> ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) : No typesetting found for \|- ( ps' -> ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) with typecode \|-
18	17	imp32	Could not format ( ( ps' /\ ( i e. _om /\ suc i e. m ) ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ps' /\ ( i e. _om /\ suc i e. m ) ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) with typecode \|-
19	10 14 18	syl2an	$⊢ (τ \land (η \land ρ)) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)$
20	9 19	simplbiim	$⊢ (R FrSe A \land τ \land η \land ρ) \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)$
21	7	fnfund	$⊢ (R FrSe A \land τ \land η) \to Fun G$
22	21	bnj721	$⊢ (R FrSe A \land τ \land η \land ρ) \to Fun G$
23	6	bnj931	$⊢ f \subseteq G$
24	23	a1i	$⊢ (R FrSe A \land τ \land η \land ρ) \to f \subseteq G$
25		bnj667	$⊢ (R FrSe A \land τ \land η \land ρ) \to (τ \land η \land ρ)$
26	2	bnj564	$⊢ τ \to dom f = m$
27		eleq2	$⊢ dom f = m \to (suc i \in dom f \leftrightarrow suc i \in m)$
28	27	biimpar	$⊢ (dom f = m \land suc i \in m) \to suc i \in dom f$
29	26 13 28	syl2an	$⊢ (τ \land (η \land ρ)) \to suc i \in dom f$
30	29	3impb	$⊢ (τ \land η \land ρ) \to suc i \in dom f$
31	25 30	syl	$⊢ (R FrSe A \land τ \land η \land ρ) \to suc i \in dom f$
32	22 24 31	bnj1502	$⊢ (R FrSe A \land τ \land η \land ρ) \to G (suc i) = f (suc i)$
33	2	simp1bi	$⊢ τ \to f Fn m$
34		bnj252	$⊢ (m \in D \land n = suc m \land p \in ω \land m = suc p) \leftrightarrow (m \in D \land (n = suc m \land p \in ω \land m = suc p))$
35	34	simplbi	$⊢ (m \in D \land n = suc m \land p \in ω \land m = suc p) \to m \in D$
36	3 35	sylbi	$⊢ η \to m \in D$
37		eldifi	$⊢ m \in (ω ∖ \{\emptyset\}) \to m \in ω$
38	37 1	eleq2s	$⊢ m \in D \to m \in ω$
39		nnord	$⊢ m \in ω \to Ord m$
40	36 38 39	3syl	$⊢ η \to Ord m$
41	40	adantr	$⊢ (η \land ρ) \to Ord m$
42	41 13	jca	$⊢ (η \land ρ) \to (Ord m \land suc i \in m)$
43	33 42	anim12i	$⊢ (τ \land (η \land ρ)) \to (f Fn m \land (Ord m \land suc i \in m))$
44		fndm	$⊢ f Fn m \to dom f = m$
45		elelsuc	$⊢ suc i \in m \to suc i \in suc m$
46		ordsucelsuc	$⊢ Ord m \to (i \in m \leftrightarrow suc i \in suc m)$
47	46	biimpar	$⊢ (Ord m \land suc i \in suc m) \to i \in m$
48	45 47	sylan2	$⊢ (Ord m \land suc i \in m) \to i \in m$
49	44 48	anim12i	$⊢ (f Fn m \land (Ord m \land suc i \in m)) \to (dom f = m \land i \in m)$
50		eleq2	$⊢ dom f = m \to (i \in dom f \leftrightarrow i \in m)$
51	50	biimpar	$⊢ (dom f = m \land i \in m) \to i \in dom f$
52	43 49 51	3syl	$⊢ (τ \land (η \land ρ)) \to i \in dom f$
53	52	3impb	$⊢ (τ \land η \land ρ) \to i \in dom f$
54	25 53	syl	$⊢ (R FrSe A \land τ \land η \land ρ) \to i \in dom f$
55	22 24 54	bnj1502	$⊢ (R FrSe A \land τ \land η \land ρ) \to G (i) = f (i)$
56	55	iuneq1d	$⊢ (R FrSe A \land τ \land η \land ρ) \to ⋃_{y \in G (i)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
57	20 32 56	3eqtr4d	$⊢ (R FrSe A \land τ \land η \land ρ) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
58	57 5	eqtr4di	$⊢ (R FrSe A \land τ \land η \land ρ) \to G (suc i) = K$

Metamath Proof Explorer

Theorem bnj570

Proof