bnj548

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	bnj548.1	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj548.2	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
	bnj548.3	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
	bnj548.4	$⊢ G = f \cup \{⟨m, C⟩\}$
	bnj548.5	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
Assertion	bnj548	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to B = K$

Proof

Step	Hyp	Ref	Expression
1		bnj548.1	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
2		bnj548.2	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
3		bnj548.3	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
4		bnj548.4	$⊢ G = f \cup \{⟨m, C⟩\}$
5		bnj548.5	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
6	5	fnfund	$⊢ (R FrSe A \land τ \land σ) \to Fun G$
7	6	adantr	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to Fun G$
8	1	simp1bi	$⊢ τ \to f Fn m$
9		fndm	$⊢ f Fn m \to dom f = m$
10		eleq2	$⊢ dom f = m \to (i \in dom f \leftrightarrow i \in m)$
11	10	biimpar	$⊢ (dom f = m \land i \in m) \to i \in dom f$
12	9 11	sylan	$⊢ (f Fn m \land i \in m) \to i \in dom f$
13	8 12	sylan	$⊢ (τ \land i \in m) \to i \in dom f$
14	13	3ad2antl2	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to i \in dom f$
15	7 14	jca	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to (Fun G \land i \in dom f)$
16	4	bnj931	$⊢ f \subseteq G$
17	15 16	jctil	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to (f \subseteq G \land (Fun G \land i \in dom f))$
18		3anan12	$⊢ (Fun G \land f \subseteq G \land i \in dom f) \leftrightarrow (f \subseteq G \land (Fun G \land i \in dom f))$
19	17 18	sylibr	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to (Fun G \land f \subseteq G \land i \in dom f)$
20		funssfv	$⊢ (Fun G \land f \subseteq G \land i \in dom f) \to G (i) = f (i)$
21		iuneq1	$⊢ G (i) = f (i) \to ⋃_{y \in G (i)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
22	21	eqcomd	$⊢ G (i) = f (i) \to ⋃_{y \in f (i)} pred (y, A, R) = ⋃_{y \in G (i)} pred (y, A, R)$
23	22 2 3	3eqtr4g	$⊢ G (i) = f (i) \to B = K$
24	19 20 23	3syl	$⊢ ((R FrSe A \land τ \land σ) \land i \in m) \to B = K$

Metamath Proof Explorer

Theorem bnj548

Proof