bnj553

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	bnj553.1	No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
	bnj553.2	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 \|-
	bnj553.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj553.4	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
	bnj553.5	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj553.6	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
	bnj553.7	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
	bnj553.8	$⊢ G = f \cup \{⟨m, C⟩\}$
	bnj553.9	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
	bnj553.10	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
	bnj553.11	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
	bnj553.12	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
Assertion	bnj553	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to G (m) = L$

Proof

Step	Hyp	Ref	Expression
1		bnj553.1	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
2		bnj553.2	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 \|-
3		bnj553.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj553.4	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
5		bnj553.5	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
6		bnj553.6	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
7		bnj553.7	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
8		bnj553.8	$⊢ G = f \cup \{⟨m, C⟩\}$
9		bnj553.9	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
10		bnj553.10	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
11		bnj553.11	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
12		bnj553.12	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
13	12	bnj930	$⊢ (R FrSe A \land τ \land σ) \to Fun G$
14		opex	$⊢ ⟨m, C⟩ \in V$
15	14	snid	$⊢ ⟨m, C⟩ \in \{⟨m, C⟩\}$
16		elun2	$⊢ ⟨m, C⟩ \in \{⟨m, C⟩\} \to ⟨m, C⟩ \in (f \cup \{⟨m, C⟩\})$
17	15 16	ax-mp	$⊢ ⟨m, C⟩ \in (f \cup \{⟨m, C⟩\})$
18	17 8	eleqtrri	$⊢ ⟨m, C⟩ \in G$
19		funopfv	$⊢ Fun G \to (⟨m, C⟩ \in G \to G (m) = C)$
20	13 18 19	mpisyl	$⊢ (R FrSe A \land τ \land σ) \to G (m) = C$
21	20	3ad2ant1	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to G (m) = C$
22		fveq2	$⊢ p = i \to G (p) = G (i)$
23	22	bnj1113	$⊢ p = i \to ⋃_{y \in G (p)} pred (y, A, R) = ⋃_{y \in G (i)} pred (y, A, R)$
24	23 11 10	3eqtr4g	$⊢ p = i \to L = K$
25	24	3ad2ant3	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to L = K$
26	5 9 10 4 12	bnj548	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to B = K$
27	26	3adant3	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to B = K$
28		fveq2	$⊢ p = i \to f (p) = f (i)$
29	28	bnj1113	$⊢ p = i \to ⋃_{y \in f (p)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
30	9 7	eqeq12i	$⊢ B = C \leftrightarrow ⋃_{y \in f (i)} pred (y, A, R) = ⋃_{y \in f (p)} pred (y, A, R)$
31		eqcom	$⊢ ⋃_{y \in f (i)} pred (y, A, R) = ⋃_{y \in f (p)} pred (y, A, R) \leftrightarrow ⋃_{y \in f (p)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
32	30 31	bitri	$⊢ B = C \leftrightarrow ⋃_{y \in f (p)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
33	29 32	sylibr	$⊢ p = i \to B = C$
34	33	3ad2ant3	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to B = C$
35	25 27 34	3eqtr2rd	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to C = L$
36	21 35	eqtrd	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to G (m) = L$

Metamath Proof Explorer

Theorem bnj553

Proof