bnj517

Description: Technical lemma for bnj518 . 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) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj517.1	$⊢ φ \leftrightarrow F (\emptyset) = pred (X, A, R)$
	bnj517.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))$
Assertion	bnj517	$⊢ (N \in ω \land φ \land ψ) \to \forall n \in N F (n) \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		bnj517.1	$⊢ φ \leftrightarrow F (\emptyset) = pred (X, A, R)$
2		bnj517.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))$
3		fveq2	$⊢ m = \emptyset \to F (m) = F (\emptyset)$
4		simpl2	$⊢ ((N \in ω \land φ \land ψ) \land m \in N) \to φ$
5	4 1	sylib	$⊢ ((N \in ω \land φ \land ψ) \land m \in N) \to F (\emptyset) = pred (X, A, R)$
6	3 5	sylan9eqr	$⊢ (((N \in ω \land φ \land ψ) \land m \in N) \land m = \emptyset) \to F (m) = pred (X, A, R)$
7		bnj213	$⊢ pred (X, A, R) \subseteq A$
8	6 7	eqsstrdi	$⊢ (((N \in ω \land φ \land ψ) \land m \in N) \land m = \emptyset) \to F (m) \subseteq A$
9		r19.29r	$⊢ (\exists i \in ω m = suc i \land \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))) \to \exists i \in ω (m = suc i \land (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R)))$
10		eleq1	$⊢ m = suc i \to (m \in N \leftrightarrow suc i \in N)$
11	10	biimpd	$⊢ m = suc i \to (m \in N \to suc i \in N)$
12		fveqeq2	$⊢ m = suc i \to (F (m) = ⋃_{y \in F (i)} pred (y, A, R) \leftrightarrow F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))$
13		bnj213	$⊢ pred (y, A, R) \subseteq A$
14	13	rgenw	$⊢ \forall y \in F (i) pred (y, A, R) \subseteq A$
15		iunss	$⊢ ⋃_{y \in F (i)} pred (y, A, R) \subseteq A \leftrightarrow \forall y \in F (i) pred (y, A, R) \subseteq A$
16	14 15	mpbir	$⊢ ⋃_{y \in F (i)} pred (y, A, R) \subseteq A$
17		sseq1	$⊢ F (m) = ⋃_{y \in F (i)} pred (y, A, R) \to (F (m) \subseteq A \leftrightarrow ⋃_{y \in F (i)} pred (y, A, R) \subseteq A)$
18	16 17	mpbiri	$⊢ F (m) = ⋃_{y \in F (i)} pred (y, A, R) \to F (m) \subseteq A$
19	12 18	biimtrrdi	$⊢ m = suc i \to (F (suc i) = ⋃_{y \in F (i)} pred (y, A, R) \to F (m) \subseteq A)$
20	11 19	imim12d	$⊢ m = suc i \to ((suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R)) \to (m \in N \to F (m) \subseteq A))$
21	20	imp	$⊢ (m = suc i \land (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))) \to (m \in N \to F (m) \subseteq A)$
22	21	rexlimivw	$⊢ \exists i \in ω (m = suc i \land (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))) \to (m \in N \to F (m) \subseteq A)$
23	9 22	syl	$⊢ (\exists i \in ω m = suc i \land \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R))) \to (m \in N \to F (m) \subseteq A)$
24	23	ex	$⊢ \exists i \in ω m = suc i \to (\forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R)) \to (m \in N \to F (m) \subseteq A))$
25	24	com3l	$⊢ \forall i \in ω (suc i \in N \to F (suc i) = ⋃_{y \in F (i)} pred (y, A, R)) \to (m \in N \to (\exists i \in ω m = suc i \to F (m) \subseteq A))$
26	2 25	sylbi	$⊢ ψ \to (m \in N \to (\exists i \in ω m = suc i \to F (m) \subseteq A))$
27	26	3ad2ant3	$⊢ (N \in ω \land φ \land ψ) \to (m \in N \to (\exists i \in ω m = suc i \to F (m) \subseteq A))$
28	27	imp31	$⊢ (((N \in ω \land φ \land ψ) \land m \in N) \land \exists i \in ω m = suc i) \to F (m) \subseteq A$
29		simpr	$⊢ ((N \in ω \land φ \land ψ) \land m \in N) \to m \in N$
30		simpl1	$⊢ ((N \in ω \land φ \land ψ) \land m \in N) \to N \in ω$
31		elnn	$⊢ (m \in N \land N \in ω) \to m \in ω$
32	29 30 31	syl2anc	$⊢ ((N \in ω \land φ \land ψ) \land m \in N) \to m \in ω$
33		nn0suc	$⊢ m \in ω \to (m = \emptyset \lor \exists i \in ω m = suc i)$
34	32 33	syl	$⊢ ((N \in ω \land φ \land ψ) \land m \in N) \to (m = \emptyset \lor \exists i \in ω m = suc i)$
35	8 28 34	mpjaodan	$⊢ ((N \in ω \land φ \land ψ) \land m \in N) \to F (m) \subseteq A$
36	35	ralrimiva	$⊢ (N \in ω \land φ \land ψ) \to \forall m \in N F (m) \subseteq A$
37		fveq2	$⊢ m = n \to F (m) = F (n)$
38	37	sseq1d	$⊢ m = n \to (F (m) \subseteq A \leftrightarrow F (n) \subseteq A)$
39	38	cbvralvw	$⊢ \forall m \in N F (m) \subseteq A \leftrightarrow \forall n \in N F (n) \subseteq A$
40	36 39	sylib	$⊢ (N \in ω \land φ \land ψ) \to \forall n \in N F (n) \subseteq A$

Metamath Proof Explorer

Theorem bnj517

Proof