bnj865

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	bnj865.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj865.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj865.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj865.5	$⊢ χ \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
	bnj865.6	$⊢ θ \leftrightarrow (f Fn n \land φ \land ψ)$
Assertion	bnj865	$⊢ \exists w \forall n (χ \to \exists f \in w θ)$

Proof

Step	Hyp	Ref	Expression
1		bnj865.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj865.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj865.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj865.5	$⊢ χ \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
5		bnj865.6	$⊢ θ \leftrightarrow (f Fn n \land φ \land ψ)$
6	1 2 3	bnj852	$⊢ (R FrSe A \land X \in A) \to \forall n \in D \exists! f (f Fn n \land φ \land ψ)$
7		omex	$⊢ ω \in V$
8		difexg	$⊢ ω \in V \to ω ∖ \{\emptyset\} \in V$
9	7 8	ax-mp	$⊢ ω ∖ \{\emptyset\} \in V$
10	3 9	eqeltri	$⊢ D \in V$
11		raleq	$⊢ z = D \to (\forall n \in z \exists! f (f Fn n \land φ \land ψ) \leftrightarrow \forall n \in D \exists! f (f Fn n \land φ \land ψ))$
12		raleq	$⊢ z = D \to (\forall n \in z \exists f \in w (f Fn n \land φ \land ψ) \leftrightarrow \forall n \in D \exists f \in w (f Fn n \land φ \land ψ))$
13	12	exbidv	$⊢ z = D \to (\exists w \forall n \in z \exists f \in w (f Fn n \land φ \land ψ) \leftrightarrow \exists w \forall n \in D \exists f \in w (f Fn n \land φ \land ψ))$
14	11 13	imbi12d	$⊢ z = D \to ((\forall n \in z \exists! f (f Fn n \land φ \land ψ) \to \exists w \forall n \in z \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow (\forall n \in D \exists! f (f Fn n \land φ \land ψ) \to \exists w \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)))$
15		zfrep6	$⊢ \forall n \in z \exists! f (f Fn n \land φ \land ψ) \to \exists w \forall n \in z \exists f \in w (f Fn n \land φ \land ψ)$
16	10 14 15	vtocl	$⊢ \forall n \in D \exists! f (f Fn n \land φ \land ψ) \to \exists w \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)$
17	6 16	syl	$⊢ (R FrSe A \land X \in A) \to \exists w \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)$
18		19.37v	$⊢ \exists w ((R FrSe A \land X \in A) \to \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land X \in A) \to \exists w \forall n \in D \exists f \in w (f Fn n \land φ \land ψ))$
19	17 18	mpbir	$⊢ \exists w ((R FrSe A \land X \in A) \to \forall n \in D \exists f \in w (f Fn n \land φ \land ψ))$
20		df-ral	$⊢ \forall n \in D \exists f \in w (f Fn n \land φ \land ψ) \leftrightarrow \forall n (n \in D \to \exists f \in w (f Fn n \land φ \land ψ))$
21	20	imbi2i	$⊢ ((R FrSe A \land X \in A) \to \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land X \in A) \to \forall n (n \in D \to \exists f \in w (f Fn n \land φ \land ψ)))$
22		19.21v	$⊢ \forall n ((R FrSe A \land X \in A) \to (n \in D \to \exists f \in w (f Fn n \land φ \land ψ))) \leftrightarrow ((R FrSe A \land X \in A) \to \forall n (n \in D \to \exists f \in w (f Fn n \land φ \land ψ)))$
23	21 22	bitr4i	$⊢ ((R FrSe A \land X \in A) \to \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow \forall n ((R FrSe A \land X \in A) \to (n \in D \to \exists f \in w (f Fn n \land φ \land ψ)))$
24	23	exbii	$⊢ \exists w ((R FrSe A \land X \in A) \to \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow \exists w \forall n ((R FrSe A \land X \in A) \to (n \in D \to \exists f \in w (f Fn n \land φ \land ψ)))$
25		impexp	$⊢ (((R FrSe A \land X \in A) \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land X \in A) \to (n \in D \to \exists f \in w (f Fn n \land φ \land ψ)))$
26		df-3an	$⊢ (R FrSe A \land X \in A \land n \in D) \leftrightarrow ((R FrSe A \land X \in A) \land n \in D)$
27	26	bicomi	$⊢ ((R FrSe A \land X \in A) \land n \in D) \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
28	27	imbi1i	$⊢ (((R FrSe A \land X \in A) \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ))$
29	25 28	bitr3i	$⊢ ((R FrSe A \land X \in A) \to (n \in D \to \exists f \in w (f Fn n \land φ \land ψ))) \leftrightarrow ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ))$
30	29	albii	$⊢ \forall n ((R FrSe A \land X \in A) \to (n \in D \to \exists f \in w (f Fn n \land φ \land ψ))) \leftrightarrow \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ))$
31	30	exbii	$⊢ \exists w \forall n ((R FrSe A \land X \in A) \to (n \in D \to \exists f \in w (f Fn n \land φ \land ψ))) \leftrightarrow \exists w \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ))$
32	24 31	bitri	$⊢ \exists w ((R FrSe A \land X \in A) \to \forall n \in D \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow \exists w \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ))$
33	19 32	mpbi	$⊢ \exists w \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ))$
34	4	bicomi	$⊢ (R FrSe A \land X \in A \land n \in D) \leftrightarrow χ$
35	34	imbi1i	$⊢ ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow (χ \to \exists f \in w (f Fn n \land φ \land ψ))$
36	35	albii	$⊢ \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow \forall n (χ \to \exists f \in w (f Fn n \land φ \land ψ))$
37	36	exbii	$⊢ \exists w \forall n ((R FrSe A \land X \in A \land n \in D) \to \exists f \in w (f Fn n \land φ \land ψ)) \leftrightarrow \exists w \forall n (χ \to \exists f \in w (f Fn n \land φ \land ψ))$
38	33 37	mpbi	$⊢ \exists w \forall n (χ \to \exists f \in w (f Fn n \land φ \land ψ))$
39	5	rexbii	$⊢ \exists f \in w θ \leftrightarrow \exists f \in w (f Fn n \land φ \land ψ)$
40	39	imbi2i	$⊢ (χ \to \exists f \in w θ) \leftrightarrow (χ \to \exists f \in w (f Fn n \land φ \land ψ))$
41	40	albii	$⊢ \forall n (χ \to \exists f \in w θ) \leftrightarrow \forall n (χ \to \exists f \in w (f Fn n \land φ \land ψ))$
42	41	exbii	$⊢ \exists w \forall n (χ \to \exists f \in w θ) \leftrightarrow \exists w \forall n (χ \to \exists f \in w (f Fn n \land φ \land ψ))$
43	38 42	mpbir	$⊢ \exists w \forall n (χ \to \exists f \in w θ)$

Metamath Proof Explorer

Theorem bnj865

Proof