bnj944

Description: Technical lemma for bnj69 . 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	bnj944.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj944.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj944.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj944.4	No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
	bnj944.7	No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
	bnj944.10	$⊢ D = ω ∖ \{\emptyset\}$
	bnj944.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
	bnj944.13	$⊢ G = f \cup \{⟨n, C⟩\}$
	bnj944.14	$⊢ τ \leftrightarrow (f Fn n \land φ \land ψ)$
	bnj944.15	$⊢ σ \leftrightarrow (n \in D \land p = suc n \land m \in n)$
Assertion	bnj944	Could not format assertion : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj944.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj944.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj944.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj944.4	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
5		bnj944.7	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
6		bnj944.10	$⊢ D = ω ∖ \{\emptyset\}$
7		bnj944.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
8		bnj944.13	$⊢ G = f \cup \{⟨n, C⟩\}$
9		bnj944.14	$⊢ τ \leftrightarrow (f Fn n \land φ \land ψ)$
10		bnj944.15	$⊢ σ \leftrightarrow (n \in D \land p = suc n \land m \in n)$
11		simpl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to (R FrSe A \land X \in A)$
12		bnj667	$⊢ (n \in D \land f Fn n \land φ \land ψ) \to (f Fn n \land φ \land ψ)$
13	3 12	sylbi	$⊢ χ \to (f Fn n \land φ \land ψ)$
14	13 9	sylibr	$⊢ χ \to τ$
15	14	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to τ$
16	15	adantl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to τ$
17	3	bnj1232	$⊢ χ \to n \in D$
18		vex	$⊢ m \in V$
19	18	bnj216	$⊢ n = suc m \to m \in n$
20		id	$⊢ p = suc n \to p = suc n$
21	17 19 20	3anim123i	$⊢ (χ \land n = suc m \land p = suc n) \to (n \in D \land m \in n \land p = suc n)$
22		3ancomb	$⊢ (n \in D \land p = suc n \land m \in n) \leftrightarrow (n \in D \land m \in n \land p = suc n)$
23	10 22	bitri	$⊢ σ \leftrightarrow (n \in D \land m \in n \land p = suc n)$
24	21 23	sylibr	$⊢ (χ \land n = suc m \land p = suc n) \to σ$
25	24	adantl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to σ$
26		bnj253	$⊢ (R FrSe A \land X \in A \land τ \land σ) \leftrightarrow ((R FrSe A \land X \in A) \land τ \land σ)$
27	11 16 25 26	syl3anbrc	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to (R FrSe A \land X \in A \land τ \land σ)$
28	6 9 10 1 2	bnj938	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to ⋃_{y \in f (m)} pred (y, A, R) \in V$
29	7 28	eqeltrid	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to C \in V$
30	27 29	syl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to C \in V$
31		bnj658	$⊢ (n \in D \land f Fn n \land φ \land ψ) \to (n \in D \land f Fn n \land φ)$
32	3 31	sylbi	$⊢ χ \to (n \in D \land f Fn n \land φ)$
33	32	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to (n \in D \land f Fn n \land φ)$
34		simp3	$⊢ (χ \land n = suc m \land p = suc n) \to p = suc n$
35		bnj291	$⊢ (n \in D \land p = suc n \land f Fn n \land φ) \leftrightarrow ((n \in D \land f Fn n \land φ) \land p = suc n)$
36	33 34 35	sylanbrc	$⊢ (χ \land n = suc m \land p = suc n) \to (n \in D \land p = suc n \land f Fn n \land φ)$
37	36	adantl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to (n \in D \land p = suc n \land f Fn n \land φ)$
38		opeq2	$⊢ C = if (C \in V, C, \emptyset) \to ⟨n, C⟩ = ⟨n, if (C \in V, C, \emptyset)⟩$
39	38	sneqd	$⊢ C = if (C \in V, C, \emptyset) \to \{⟨n, C⟩\} = \{⟨n, if (C \in V, C, \emptyset)⟩\}$
40	39	uneq2d	$⊢ C = if (C \in V, C, \emptyset) \to f \cup \{⟨n, C⟩\} = f \cup \{⟨n, if (C \in V, C, \emptyset)⟩\}$
41	8 40	eqtrid	$⊢ C = if (C \in V, C, \emptyset) \to G = f \cup \{⟨n, if (C \in V, C, \emptyset)⟩\}$
42	41	sbceq1d	Could not format ( C = if ( C e. _V , C , (/) ) -> ( [. G / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) : No typesetting found for \|- ( C = if ( C e. _V , C , (/) ) -> ( [. G / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) with typecode \|-
43	5 42	bitrid	Could not format ( C = if ( C e. _V , C , (/) ) -> ( ph" <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) : No typesetting found for \|- ( C = if ( C e. _V , C , (/) ) -> ( ph" <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) with typecode \|-
44	43	imbi2d	Could not format ( C = if ( C e. _V , C , (/) ) -> ( ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) <-> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) ) : No typesetting found for \|- ( C = if ( C e. _V , C , (/) ) -> ( ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) <-> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) ) with typecode \|-
45		biid	Could not format ( [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) : No typesetting found for \|- ( [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) with typecode \|-
46		eqid	$⊢ f \cup \{⟨n, if (C \in V, C, \emptyset)⟩\} = f \cup \{⟨n, if (C \in V, C, \emptyset)⟩\}$
47		0ex	$⊢ \emptyset \in V$
48	47	elimel	$⊢ if (C \in V, C, \emptyset) \in V$
49	1 4 45 6 46 48	bnj929	Could not format ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) : No typesetting found for \|- ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) with typecode \|-
50	44 49	dedth	Could not format ( C e. _V -> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) ) : No typesetting found for \|- ( C e. _V -> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) ) with typecode \|-
51	30 37 50	sylc	Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) with typecode \|-

Metamath Proof Explorer

Theorem bnj944

Proof