dfac5lem5

	Ref	Expression
Hypotheses	dfac5lem.1	$⊢ A = \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
	dfac5lem.2	$⊢ B = ⋃ A \cap y$
	dfac5lem.3	$⊢ φ \leftrightarrow \forall x ((\forall z \in x z \neq \emptyset \land \forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in x \exists! v v \in (z \cap y))$
Assertion	dfac5lem5	$⊢ φ \to \exists f \forall w \in h (w \neq \emptyset \to f (w) \in w)$

Proof

Step	Hyp	Ref	Expression
1		dfac5lem.1	$⊢ A = \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
2		dfac5lem.2	$⊢ B = ⋃ A \cap y$
3		dfac5lem.3	$⊢ φ \leftrightarrow \forall x ((\forall z \in x z \neq \emptyset \land \forall z \in x \forall w \in x (z \neq w \to z \cap w = \emptyset)) \to \exists y \forall z \in x \exists! v v \in (z \cap y))$
4	1 2 3	dfac5lem4	$⊢ φ \to \exists y \forall z \in A \exists! v v \in (z \cap y)$
5		simpr	$⊢ (w \neq \emptyset \land w \in h) \to w \in h$
6	5	a1i	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to ((w \neq \emptyset \land w \in h) \to w \in h)$
7		ineq1	$⊢ z = \{w\} \times w \to z \cap y = (\{w\} \times w) \cap y$
8	7	eleq2d	$⊢ z = \{w\} \times w \to (v \in (z \cap y) \leftrightarrow v \in ((\{w\} \times w) \cap y))$
9	8	eubidv	$⊢ z = \{w\} \times w \to (\exists! v v \in (z \cap y) \leftrightarrow \exists! v v \in ((\{w\} \times w) \cap y))$
10	9	rspccv	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to (\{w\} \times w \in A \to \exists! v v \in ((\{w\} \times w) \cap y))$
11	1	dfac5lem3	$⊢ \{w\} \times w \in A \leftrightarrow (w \neq \emptyset \land w \in h)$
12		dfac5lem1	$⊢ \exists! v v \in ((\{w\} \times w) \cap y) \leftrightarrow \exists! g (g \in w \land ⟨w, g⟩ \in y)$
13	10 11 12	3imtr3g	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to ((w \neq \emptyset \land w \in h) \to \exists! g (g \in w \land ⟨w, g⟩ \in y))$
14	6 13	jcad	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to ((w \neq \emptyset \land w \in h) \to (w \in h \land \exists! g (g \in w \land ⟨w, g⟩ \in y)))$
15	2	eleq2i	$⊢ ⟨w, g⟩ \in B \leftrightarrow ⟨w, g⟩ \in (⋃ A \cap y)$
16		elin	$⊢ ⟨w, g⟩ \in (⋃ A \cap y) \leftrightarrow (⟨w, g⟩ \in ⋃ A \land ⟨w, g⟩ \in y)$
17	1	dfac5lem2	$⊢ ⟨w, g⟩ \in ⋃ A \leftrightarrow (w \in h \land g \in w)$
18	17	anbi1i	$⊢ (⟨w, g⟩ \in ⋃ A \land ⟨w, g⟩ \in y) \leftrightarrow ((w \in h \land g \in w) \land ⟨w, g⟩ \in y)$
19		anass	$⊢ ((w \in h \land g \in w) \land ⟨w, g⟩ \in y) \leftrightarrow (w \in h \land (g \in w \land ⟨w, g⟩ \in y))$
20	18 19	bitri	$⊢ (⟨w, g⟩ \in ⋃ A \land ⟨w, g⟩ \in y) \leftrightarrow (w \in h \land (g \in w \land ⟨w, g⟩ \in y))$
21	15 16 20	3bitri	$⊢ ⟨w, g⟩ \in B \leftrightarrow (w \in h \land (g \in w \land ⟨w, g⟩ \in y))$
22	21	eubii	$⊢ \exists! g ⟨w, g⟩ \in B \leftrightarrow \exists! g (w \in h \land (g \in w \land ⟨w, g⟩ \in y))$
23		euanv	$⊢ \exists! g (w \in h \land (g \in w \land ⟨w, g⟩ \in y)) \leftrightarrow (w \in h \land \exists! g (g \in w \land ⟨w, g⟩ \in y))$
24	22 23	bitr2i	$⊢ (w \in h \land \exists! g (g \in w \land ⟨w, g⟩ \in y)) \leftrightarrow \exists! g ⟨w, g⟩ \in B$
25	14 24	imbitrdi	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to ((w \neq \emptyset \land w \in h) \to \exists! g ⟨w, g⟩ \in B)$
26		euex	$⊢ \exists! g ⟨w, g⟩ \in B \to \exists g ⟨w, g⟩ \in B$
27		nfeu1	$⊢ Ⅎ g \exists! g ⟨w, g⟩ \in B$
28		nfv	$⊢ Ⅎ g B (w) \in w$
29	27 28	nfim	$⊢ Ⅎ g (\exists! g ⟨w, g⟩ \in B \to B (w) \in w)$
30	21	simprbi	$⊢ ⟨w, g⟩ \in B \to (g \in w \land ⟨w, g⟩ \in y)$
31	30	simpld	$⊢ ⟨w, g⟩ \in B \to g \in w$
32		tz6.12	$⊢ (⟨w, g⟩ \in B \land \exists! g ⟨w, g⟩ \in B) \to B (w) = g$
33	32	eleq1d	$⊢ (⟨w, g⟩ \in B \land \exists! g ⟨w, g⟩ \in B) \to (B (w) \in w \leftrightarrow g \in w)$
34	33	biimparc	$⊢ (g \in w \land (⟨w, g⟩ \in B \land \exists! g ⟨w, g⟩ \in B)) \to B (w) \in w$
35	34	exp32	$⊢ g \in w \to (⟨w, g⟩ \in B \to (\exists! g ⟨w, g⟩ \in B \to B (w) \in w))$
36	31 35	mpcom	$⊢ ⟨w, g⟩ \in B \to (\exists! g ⟨w, g⟩ \in B \to B (w) \in w)$
37	29 36	exlimi	$⊢ \exists g ⟨w, g⟩ \in B \to (\exists! g ⟨w, g⟩ \in B \to B (w) \in w)$
38	26 37	mpcom	$⊢ \exists! g ⟨w, g⟩ \in B \to B (w) \in w$
39	25 38	syl6	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to ((w \neq \emptyset \land w \in h) \to B (w) \in w)$
40	39	expcomd	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to (w \in h \to (w \neq \emptyset \to B (w) \in w))$
41	40	ralrimiv	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to \forall w \in h (w \neq \emptyset \to B (w) \in w)$
42		vex	$⊢ y \in V$
43	42	inex2	$⊢ ⋃ A \cap y \in V$
44	2 43	eqeltri	$⊢ B \in V$
45		fveq1	$⊢ f = B \to f (w) = B (w)$
46	45	eleq1d	$⊢ f = B \to (f (w) \in w \leftrightarrow B (w) \in w)$
47	46	imbi2d	$⊢ f = B \to ((w \neq \emptyset \to f (w) \in w) \leftrightarrow (w \neq \emptyset \to B (w) \in w))$
48	47	ralbidv	$⊢ f = B \to (\forall w \in h (w \neq \emptyset \to f (w) \in w) \leftrightarrow \forall w \in h (w \neq \emptyset \to B (w) \in w))$
49	44 48	spcev	$⊢ \forall w \in h (w \neq \emptyset \to B (w) \in w) \to \exists f \forall w \in h (w \neq \emptyset \to f (w) \in w)$
50	41 49	syl	$⊢ \forall z \in A \exists! v v \in (z \cap y) \to \exists f \forall w \in h (w \neq \emptyset \to f (w) \in w)$
51	50	exlimiv	$⊢ \exists y \forall z \in A \exists! v v \in (z \cap y) \to \exists f \forall w \in h (w \neq \emptyset \to f (w) \in w)$
52	4 51	syl	$⊢ φ \to \exists f \forall w \in h (w \neq \emptyset \to f (w) \in w)$

Metamath Proof Explorer

Theorem dfac5lem5

Proof