aceq3lem

Description: Lemma for dfac3 . (Contributed by NM, 2-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Hypothesis	aceq3lem.1	$⊢ F = (w \in dom y ⟼ f (\{u \| w y u\}))$
	Assertion	aceq3lem	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists f (f \subseteq y \land f Fn dom y)$

Proof

Step	Hyp	Ref	Expression
1		aceq3lem.1	$⊢ F = (w \in dom y ⟼ f (\{u \| w y u\}))$
2		vex	$⊢ y \in V$
3	2	rnex	$⊢ ran y \in V$
4	3	pwex	$⊢ 𝒫 ran y \in V$
5		raleq	$⊢ x = 𝒫 ran y \to (\forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z))$
6	5	exbidv	$⊢ x = 𝒫 ran y \to (\exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \leftrightarrow \exists f \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z))$
7	4 6	spcv	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists f \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z)$
8		df-mpt	$⊢ (w \in dom y ⟼ f (\{u \| w y u\})) = \{⟨w, h⟩ \| (w \in dom y \land h = f (\{u \| w y u\}))\}$
9	1 8	eqtri	$⊢ F = \{⟨w, h⟩ \| (w \in dom y \land h = f (\{u \| w y u\}))\}$
10		vex	$⊢ w \in V$
11	10	eldm	$⊢ w \in dom y \leftrightarrow \exists u w y u$
12		abn0	$⊢ \{u \| w y u\} \neq \emptyset \leftrightarrow \exists u w y u$
13	11 12	bitr4i	$⊢ w \in dom y \leftrightarrow \{u \| w y u\} \neq \emptyset$
14		vex	$⊢ u \in V$
15	10 14	brelrn	$⊢ w y u \to u \in ran y$
16	15	abssi	$⊢ \{u \| w y u\} \subseteq ran y$
17	3 16	elpwi2	$⊢ \{u \| w y u\} \in 𝒫 ran y$
18		neeq1	$⊢ z = \{u \| w y u\} \to (z \neq \emptyset \leftrightarrow \{u \| w y u\} \neq \emptyset)$
19		fveq2	$⊢ z = \{u \| w y u\} \to f (z) = f (\{u \| w y u\})$
20		id	$⊢ z = \{u \| w y u\} \to z = \{u \| w y u\}$
21	19 20	eleq12d	$⊢ z = \{u \| w y u\} \to (f (z) \in z \leftrightarrow f (\{u \| w y u\}) \in \{u \| w y u\})$
22	18 21	imbi12d	$⊢ z = \{u \| w y u\} \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (\{u \| w y u\} \neq \emptyset \to f (\{u \| w y u\}) \in \{u \| w y u\}))$
23	22	rspcv	$⊢ \{u \| w y u\} \in 𝒫 ran y \to (\forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to (\{u \| w y u\} \neq \emptyset \to f (\{u \| w y u\}) \in \{u \| w y u\}))$
24	17 23	ax-mp	$⊢ \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to (\{u \| w y u\} \neq \emptyset \to f (\{u \| w y u\}) \in \{u \| w y u\})$
25	13 24	syl5bi	$⊢ \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to (w \in dom y \to f (\{u \| w y u\}) \in \{u \| w y u\})$
26	25	imp	$⊢ (\forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \land w \in dom y) \to f (\{u \| w y u\}) \in \{u \| w y u\}$
27		fvex	$⊢ f (\{u \| w y u\}) \in V$
28		breq2	$⊢ z = f (\{u \| w y u\}) \to (w y z \leftrightarrow w y f (\{u \| w y u\}))$
29		breq2	$⊢ u = z \to (w y u \leftrightarrow w y z)$
30	29	cbvabv	$⊢ \{u \| w y u\} = \{z \| w y z\}$
31	27 28 30	elab2	$⊢ f (\{u \| w y u\}) \in \{u \| w y u\} \leftrightarrow w y f (\{u \| w y u\})$
32	26 31	sylib	$⊢ (\forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \land w \in dom y) \to w y f (\{u \| w y u\})$
33		breq2	$⊢ h = f (\{u \| w y u\}) \to (w y h \leftrightarrow w y f (\{u \| w y u\}))$
34	32 33	syl5ibrcom	$⊢ (\forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \land w \in dom y) \to (h = f (\{u \| w y u\}) \to w y h)$
35	34	expimpd	$⊢ \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to ((w \in dom y \land h = f (\{u \| w y u\})) \to w y h)$
36	35	ssopab2dv	$⊢ \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to \{⟨w, h⟩ \| (w \in dom y \land h = f (\{u \| w y u\}))\} \subseteq \{⟨w, h⟩ \| w y h\}$
37		opabss	$⊢ \{⟨w, h⟩ \| w y h\} \subseteq y$
38	36 37	sstrdi	$⊢ \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to \{⟨w, h⟩ \| (w \in dom y \land h = f (\{u \| w y u\}))\} \subseteq y$
39	9 38	eqsstrid	$⊢ \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to F \subseteq y$
40	27 1	fnmpti	$⊢ F Fn dom y$
41	2	ssex	$⊢ F \subseteq y \to F \in V$
42	41	adantr	$⊢ (F \subseteq y \land F Fn dom y) \to F \in V$
43		sseq1	$⊢ g = F \to (g \subseteq y \leftrightarrow F \subseteq y)$
44		fneq1	$⊢ g = F \to (g Fn dom y \leftrightarrow F Fn dom y)$
45	43 44	anbi12d	$⊢ g = F \to ((g \subseteq y \land g Fn dom y) \leftrightarrow (F \subseteq y \land F Fn dom y))$
46	45	spcegv	$⊢ F \in V \to ((F \subseteq y \land F Fn dom y) \to \exists g (g \subseteq y \land g Fn dom y))$
47	42 46	mpcom	$⊢ (F \subseteq y \land F Fn dom y) \to \exists g (g \subseteq y \land g Fn dom y)$
48	39 40 47	sylancl	$⊢ \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to \exists g (g \subseteq y \land g Fn dom y)$
49	48	exlimiv	$⊢ \exists f \forall z \in 𝒫 ran y (z \neq \emptyset \to f (z) \in z) \to \exists g (g \subseteq y \land g Fn dom y)$
50	7 49	syl	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists g (g \subseteq y \land g Fn dom y)$
51		sseq1	$⊢ g = f \to (g \subseteq y \leftrightarrow f \subseteq y)$
52		fneq1	$⊢ g = f \to (g Fn dom y \leftrightarrow f Fn dom y)$
53	51 52	anbi12d	$⊢ g = f \to ((g \subseteq y \land g Fn dom y) \leftrightarrow (f \subseteq y \land f Fn dom y))$
54	53	cbvexvw	$⊢ \exists g (g \subseteq y \land g Fn dom y) \leftrightarrow \exists f (f \subseteq y \land f Fn dom y)$
55	50 54	sylib	$⊢ \forall x \exists f \forall z \in x (z \neq \emptyset \to f (z) \in z) \to \exists f (f \subseteq y \land f Fn dom y)$

Metamath Proof Explorer

Theorem aceq3lem

Proof