bnj1052

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	bnj1052.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj1052.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1052.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1052.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
	bnj1052.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
	bnj1052.6	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
	bnj1052.7	$⊢ D = ω ∖ \{\emptyset\}$
	bnj1052.8	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj1052.9	$⊢ η \leftrightarrow ((θ \land τ \land χ \land ζ) \to z \in B)$
	bnj1052.10	$⊢ ρ \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} η)$
	bnj1052.37	$⊢ (θ \land τ \land χ \land ζ) \to (E Fr n \land \forall i \in n (ρ \to η))$
Assertion	bnj1052	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		bnj1052.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1052.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1052.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1052.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
5		bnj1052.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
6		bnj1052.6	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
7		bnj1052.7	$⊢ D = ω ∖ \{\emptyset\}$
8		bnj1052.8	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
9		bnj1052.9	$⊢ η \leftrightarrow ((θ \land τ \land χ \land ζ) \to z \in B)$
10		bnj1052.10	$⊢ ρ \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} η)$
11		bnj1052.37	$⊢ (θ \land τ \land χ \land ζ) \to (E Fr n \land \forall i \in n (ρ \to η))$
12		19.23vv	$⊢ \forall n \forall i ((θ \land τ \land χ \land ζ) \to z \in B) \leftrightarrow (\exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B)$
13	12	albii	$⊢ \forall f \forall n \forall i ((θ \land τ \land χ \land ζ) \to z \in B) \leftrightarrow \forall f (\exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B)$
14		19.23v	$⊢ \forall f (\exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B) \leftrightarrow (\exists f \exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B)$
15	13 14	bitri	$⊢ \forall f \forall n \forall i ((θ \land τ \land χ \land ζ) \to z \in B) \leftrightarrow (\exists f \exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B)$
16		vex	$⊢ n \in V$
17	16 10	bnj110	$⊢ (E Fr n \land \forall i \in n (ρ \to η)) \to \forall i \in n η$
18	6 9	bnj1049	$⊢ \forall i \in n η \leftrightarrow \forall i η$
19	17 18	sylib	$⊢ (E Fr n \land \forall i \in n (ρ \to η)) \to \forall i η$
20	19	19.21bi	$⊢ (E Fr n \land \forall i \in n (ρ \to η)) \to η$
21	20 9	sylib	$⊢ (E Fr n \land \forall i \in n (ρ \to η)) \to ((θ \land τ \land χ \land ζ) \to z \in B)$
22	11 21	mpcom	$⊢ (θ \land τ \land χ \land ζ) \to z \in B$
23	22	gen2	$⊢ \forall n \forall i ((θ \land τ \land χ \land ζ) \to z \in B)$
24	15 23	mpgbi	$⊢ \exists f \exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B$
25	1 2 3 4 5 6 7 8 24	bnj1034	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$

Metamath Proof Explorer

Theorem bnj1052

Proof