This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj121

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	bnj121.1	$⊢ ζ \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
		bnj121.2	No typesetting found for \|- ( ze' <-> [. 1o / n ]. ze ) with typecode \|-
		bnj121.3	No typesetting found for \|- ( ph' <-> [. 1o / n ]. ph ) with typecode \|-
		bnj121.4	No typesetting found for \|- ( ps' <-> [. 1o / n ]. ps ) with typecode \|-
	Assertion	bnj121	Could not format assertion : No typesetting found for \|- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj121.1	$⊢ ζ \leftrightarrow ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
2		bnj121.2	Could not format ( ze' <-> [. 1o / n ]. ze ) : No typesetting found for \|- ( ze' <-> [. 1o / n ]. ze ) with typecode \|-
3		bnj121.3	Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. 1o / n ]. ph ) with typecode \|-
4		bnj121.4	Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. 1o / n ]. ps ) with typecode \|-
5	1	sbcbii	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ζ \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ))$
6		bnj105	$⊢ 1_{𝑜} \in V$
7	6	bnj90	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} f Fn n \leftrightarrow f Fn 1_{𝑜}$
8	7	bicomi	$⊢ f Fn 1_{𝑜} \leftrightarrow \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} f Fn n$
9	8 3 4	3anbi123i	Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) : No typesetting found for \|- ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) with typecode \|-
10		sbc3an	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} (f Fn n \land φ \land ψ) \leftrightarrow (\underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} f Fn n \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} φ \land \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ψ)$
11	9 10	bitr4i	Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) : No typesetting found for \|- ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) with typecode \|-
12	11	imbi2i	Could not format ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) ) with typecode \|-
13		nfv	$⊢ Ⅎ n (R FrSe A \land x \in A)$
14	13	sbc19.21g	$⊢ 1_{𝑜} \in V \to (\underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} (f Fn n \land φ \land ψ)))$
15	6 14	ax-mp	$⊢ \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} ((R FrSe A \land x \in A) \to (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land x \in A) \to \underset{˙}{[} 1_{𝑜} / n \underset{˙}{]} (f Fn n \land φ \land ψ))$
16	12 15	bitr4i	Could not format ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) ) with typecode \|-
17	5 2 16	3bitr4i	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 \|-