bnj545

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	bnj545.1	No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
	bnj545.2	$⊢ D = ω ∖ \{\emptyset\}$
	bnj545.3	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
	bnj545.4	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj545.5	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
	bnj545.6	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
	bnj545.7	No typesetting found for \|- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
Assertion	bnj545	Could not format assertion : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ si ) -> ph" ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj545.1	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
2		bnj545.2	$⊢ D = ω ∖ \{\emptyset\}$
3		bnj545.3	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
4		bnj545.4	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
5		bnj545.5	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
6		bnj545.6	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
7		bnj545.7	Could not format ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
8	4	simp1bi	$⊢ τ \to f Fn m$
9	5	simp1bi	$⊢ σ \to m \in D$
10	8 9	anim12i	$⊢ (τ \land σ) \to (f Fn m \land m \in D)$
11	10	3adant1	$⊢ (R FrSe A \land τ \land σ) \to (f Fn m \land m \in D)$
12	2	bnj529	$⊢ m \in D \to \emptyset \in m$
13		fndm	$⊢ f Fn m \to dom f = m$
14		eleq2	$⊢ dom f = m \to (\emptyset \in dom f \leftrightarrow \emptyset \in m)$
15	14	biimparc	$⊢ (\emptyset \in m \land dom f = m) \to \emptyset \in dom f$
16	12 13 15	syl2anr	$⊢ (f Fn m \land m \in D) \to \emptyset \in dom f$
17	11 16	syl	$⊢ (R FrSe A \land τ \land σ) \to \emptyset \in dom f$
18	6	fnfund	$⊢ (R FrSe A \land τ \land σ) \to Fun G$
19	17 18	jca	$⊢ (R FrSe A \land τ \land σ) \to (\emptyset \in dom f \land Fun G)$
20	3	bnj931	$⊢ f \subseteq G$
21	19 20	jctil	$⊢ (R FrSe A \land τ \land σ) \to (f \subseteq G \land (\emptyset \in dom f \land Fun G))$
22		df-3an	$⊢ (\emptyset \in dom f \land Fun G \land f \subseteq G) \leftrightarrow ((\emptyset \in dom f \land Fun G) \land f \subseteq G)$
23		3anrot	$⊢ (\emptyset \in dom f \land Fun G \land f \subseteq G) \leftrightarrow (Fun G \land f \subseteq G \land \emptyset \in dom f)$
24		ancom	$⊢ ((\emptyset \in dom f \land Fun G) \land f \subseteq G) \leftrightarrow (f \subseteq G \land (\emptyset \in dom f \land Fun G))$
25	22 23 24	3bitr3i	$⊢ (Fun G \land f \subseteq G \land \emptyset \in dom f) \leftrightarrow (f \subseteq G \land (\emptyset \in dom f \land Fun G))$
26	21 25	sylibr	$⊢ (R FrSe A \land τ \land σ) \to (Fun G \land f \subseteq G \land \emptyset \in dom f)$
27		funssfv	$⊢ (Fun G \land f \subseteq G \land \emptyset \in dom f) \to G (\emptyset) = f (\emptyset)$
28	26 27	syl	$⊢ (R FrSe A \land τ \land σ) \to G (\emptyset) = f (\emptyset)$
29	4	simp2bi	Could not format ( ta -> ph' ) : No typesetting found for \|- ( ta -> ph' ) with typecode \|-
30	29	3ad2ant2	Could not format ( ( R _FrSe A /\ ta /\ si ) -> ph' ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ si ) -> ph' ) with typecode \|-
31		eqtr	$⊢ (G (\emptyset) = f (\emptyset) \land f (\emptyset) = pred (x, A, R)) \to G (\emptyset) = pred (x, A, R)$
32	1 31	sylan2b	Could not format ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
33	32 7	sylibr	Could not format ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ph" ) : No typesetting found for \|- ( ( ( G ` (/) ) = ( f ` (/) ) /\ ph' ) -> ph" ) with typecode \|-
34	28 30 33	syl2anc	Could not format ( ( R _FrSe A /\ ta /\ si ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ si ) -> ph" ) with typecode \|-

Metamath Proof Explorer

Theorem bnj545

Proof