bnj150

Description: Technical lemma for bnj151 . 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	bnj150.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj150.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj150.3	$⊢ ζ \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
	bnj150.4	No typesetting found for \|- ( ph' <-> [. 1o / n ]. ph ) with typecode \|-
	bnj150.5	No typesetting found for \|- ( ps' <-> [. 1o / n ]. ps ) with typecode \|-
	bnj150.6	No typesetting found for \|- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode \|-
	bnj150.7	No typesetting found for \|- ( ze' <-> [. 1o / n ]. ze ) with typecode \|-
	bnj150.8	$⊢ F = \{⟨\emptyset, pred (x, A, R)⟩\}$
	bnj150.9	No typesetting found for \|- ( ph" <-> [. F / f ]. ph' ) with typecode \|-
	bnj150.10	No typesetting found for \|- ( ps" <-> [. F / f ]. ps' ) with typecode \|-
	bnj150.11	No typesetting found for \|- ( ze" <-> [. F / f ]. ze' ) with typecode \|-
Assertion	bnj150	Could not format assertion : No typesetting found for \|- th0 with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj150.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj150.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj150.3	$⊢ ζ \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
4		bnj150.4	Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. 1o / n ]. ph ) with typecode \|-
5		bnj150.5	Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. 1o / n ]. ps ) with typecode \|-
6		bnj150.6	Could not format ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode \|-
7		bnj150.7	Could not format ( ze' <-> [. 1o / n ]. ze ) : No typesetting found for \|- ( ze' <-> [. 1o / n ]. ze ) with typecode \|-
8		bnj150.8	$⊢ F = \{⟨\emptyset, pred (x, A, R)⟩\}$
9		bnj150.9	Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. F / f ]. ph' ) with typecode \|-
10		bnj150.10	Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. F / f ]. ps' ) with typecode \|-
11		bnj150.11	Could not format ( ze" <-> [. F / f ]. ze' ) : No typesetting found for \|- ( ze" <-> [. F / f ]. ze' ) with typecode \|-
12	8	bnj95	$⊢ F \in V$
13		sbceq1a	Could not format ( f = F -> ( ze' <-> [. F / f ]. ze' ) ) : No typesetting found for \|- ( f = F -> ( ze' <-> [. F / f ]. ze' ) ) with typecode \|-
14	13 11	bitr4di	Could not format ( f = F -> ( ze' <-> ze" ) ) : No typesetting found for \|- ( f = F -> ( ze' <-> ze" ) ) with typecode \|-
15		0ex	$⊢ \emptyset \in V$
16		bnj93	$⊢ (R FrSe A \land x \in A) \to pred (x, A, R) \in V$
17		funsng	$⊢ (\emptyset \in V \land pred (x, A, R) \in V) \to Fun \{⟨\emptyset, pred (x, A, R)⟩\}$
18	15 16 17	sylancr	$⊢ (R FrSe A \land x \in A) \to Fun \{⟨\emptyset, pred (x, A, R)⟩\}$
19	8	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨\emptyset, pred (x, A, R)⟩\}$
20	18 19	sylibr	$⊢ (R FrSe A \land x \in A) \to Fun F$
21	8	bnj96	$⊢ (R FrSe A \land x \in A) \to dom F = 1_{𝑜}$
22	20 21	bnj1422	$⊢ (R FrSe A \land x \in A) \to F Fn 1_{𝑜}$
23	8	bnj97	$⊢ (R FrSe A \land x \in A) \to F (\emptyset) = pred (x, A, R)$
24	1 4 9 8	bnj125	Could not format ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
25	23 24	sylibr	Could not format ( ( R _FrSe A /\ x e. A ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A ) -> ph" ) with typecode \|-
26	22 25	jca	Could not format ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" ) ) with typecode \|-
27		bnj98	$⊢ \forall i \in ω (suc i \in 1_{𝑜} \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))$
28	2 5 10 8	bnj126	Could not format ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) with typecode \|-
29	27 28	mpbir	Could not format ps" : No typesetting found for \|- ps" with typecode \|-
30		df-3an	Could not format ( ( F Fn 1o /\ ph" /\ ps" ) <-> ( ( F Fn 1o /\ ph" ) /\ ps" ) ) : No typesetting found for \|- ( ( F Fn 1o /\ ph" /\ ps" ) <-> ( ( F Fn 1o /\ ph" ) /\ ps" ) ) with typecode \|-
31	26 29 30	sylanblrc	Could not format ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) with typecode \|-
32	3 7 4 5	bnj121	Could not format ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode \|-
33	8 9 10 11 32	bnj124	Could not format ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for \|- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode \|-
34	31 33	mpbir	Could not format ze" : No typesetting found for \|- ze" with typecode \|-
35	12 14 34	ceqsexv2d	Could not format E. f ze' : No typesetting found for \|- E. f ze' with typecode \|-
36		19.37v	Could not format ( E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode \|-
37	6 36	bitr4i	Could not format ( th0 <-> E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( th0 <-> E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode \|-
38	37 32	bnj133	Could not format ( th0 <-> E. f ze' ) : No typesetting found for \|- ( th0 <-> E. f ze' ) with typecode \|-
39	35 38	mpbir	Could not format th0 : No typesetting found for \|- th0 with typecode \|-

Metamath Proof Explorer

Theorem bnj150

Proof