bnj1053

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

Proof

Step	Hyp	Ref	Expression
1		bnj1053.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1053.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1053.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1053.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
5		bnj1053.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
6		bnj1053.6	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
7		bnj1053.7	$⊢ D = ω ∖ \{\emptyset\}$
8		bnj1053.8	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
9		bnj1053.9	$⊢ η \leftrightarrow ((θ \land τ \land χ \land ζ) \to z \in B)$
10		bnj1053.10	$⊢ ρ \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} η)$
11		bnj1053.37	$⊢ (θ \land τ \land χ \land ζ) \to \forall i \in n (ρ \to η)$
12	7	bnj923	$⊢ n \in D \to n \in ω$
13		nnord	$⊢ n \in ω \to Ord n$
14		ordfr	$⊢ Ord n \to E Fr n$
15	12 13 14	3syl	$⊢ n \in D \to E Fr n$
16	3 15	bnj769	$⊢ χ \to E Fr n$
17	16	bnj707	$⊢ (θ \land τ \land χ \land ζ) \to E Fr n$
18	17 11	jca	$⊢ (θ \land τ \land χ \land ζ) \to (E Fr n \land \forall i \in n (ρ \to η))$
19	1 2 3 4 5 6 7 8 9 10 18	bnj1052	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$

Metamath Proof Explorer

Theorem bnj1053

Proof