kmlem2

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004)

		Ref	Expression
	Assertion	kmlem2	$⊢ \exists y \forall z \in x (φ \to \exists! w w \in (z \cap y)) \leftrightarrow \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y)))$

Proof

Step	Hyp	Ref	Expression
1		ineq2	$⊢ y = v \to z \cap y = z \cap v$
2	1	eleq2d	$⊢ y = v \to (w \in (z \cap y) \leftrightarrow w \in (z \cap v))$
3	2	eubidv	$⊢ y = v \to (\exists! w w \in (z \cap y) \leftrightarrow \exists! w w \in (z \cap v))$
4	3	imbi2d	$⊢ y = v \to ((φ \to \exists! w w \in (z \cap y)) \leftrightarrow (φ \to \exists! w w \in (z \cap v)))$
5	4	ralbidv	$⊢ y = v \to (\forall z \in x (φ \to \exists! w w \in (z \cap y)) \leftrightarrow \forall z \in x (φ \to \exists! w w \in (z \cap v)))$
6	5	cbvexvw	$⊢ \exists y \forall z \in x (φ \to \exists! w w \in (z \cap y)) \leftrightarrow \exists v \forall z \in x (φ \to \exists! w w \in (z \cap v))$
7		indi	$⊢ z \cap (v \cup \{u\}) = (z \cap v) \cup (z \cap \{u\})$
8		elssuni	$⊢ z \in x \to z \subseteq ⋃ x$
9	8	ssneld	$⊢ z \in x \to (\neg u \in ⋃ x \to \neg u \in z)$
10		disjsn	$⊢ z \cap \{u\} = \emptyset \leftrightarrow \neg u \in z$
11	9 10	imbitrrdi	$⊢ z \in x \to (\neg u \in ⋃ x \to z \cap \{u\} = \emptyset)$
12	11	impcom	$⊢ (\neg u \in ⋃ x \land z \in x) \to z \cap \{u\} = \emptyset$
13	12	uneq2d	$⊢ (\neg u \in ⋃ x \land z \in x) \to (z \cap v) \cup (z \cap \{u\}) = (z \cap v) \cup \emptyset$
14		un0	$⊢ (z \cap v) \cup \emptyset = z \cap v$
15	13 14	eqtrdi	$⊢ (\neg u \in ⋃ x \land z \in x) \to (z \cap v) \cup (z \cap \{u\}) = z \cap v$
16	7 15	eqtr2id	$⊢ (\neg u \in ⋃ x \land z \in x) \to z \cap v = z \cap (v \cup \{u\})$
17	16	eleq2d	$⊢ (\neg u \in ⋃ x \land z \in x) \to (w \in (z \cap v) \leftrightarrow w \in (z \cap (v \cup \{u\})))$
18	17	eubidv	$⊢ (\neg u \in ⋃ x \land z \in x) \to (\exists! w w \in (z \cap v) \leftrightarrow \exists! w w \in (z \cap (v \cup \{u\})))$
19	18	imbi2d	$⊢ (\neg u \in ⋃ x \land z \in x) \to ((φ \to \exists! w w \in (z \cap v)) \leftrightarrow (φ \to \exists! w w \in (z \cap (v \cup \{u\}))))$
20	19	ralbidva	$⊢ \neg u \in ⋃ x \to (\forall z \in x (φ \to \exists! w w \in (z \cap v)) \leftrightarrow \forall z \in x (φ \to \exists! w w \in (z \cap (v \cup \{u\}))))$
21		vsnid	$⊢ u \in \{u\}$
22	21	olci	$⊢ (u \in v \lor u \in \{u\})$
23		elun	$⊢ u \in (v \cup \{u\}) \leftrightarrow (u \in v \lor u \in \{u\})$
24	22 23	mpbir	$⊢ u \in (v \cup \{u\})$
25		elssuni	$⊢ v \cup \{u\} \in x \to v \cup \{u\} \subseteq ⋃ x$
26	25	sseld	$⊢ v \cup \{u\} \in x \to (u \in (v \cup \{u\}) \to u \in ⋃ x)$
27	24 26	mpi	$⊢ v \cup \{u\} \in x \to u \in ⋃ x$
28	27	con3i	$⊢ \neg u \in ⋃ x \to \neg v \cup \{u\} \in x$
29	28	biantrurd	$⊢ \neg u \in ⋃ x \to (\forall z \in x (φ \to \exists! w w \in (z \cap (v \cup \{u\}))) \leftrightarrow (\neg v \cup \{u\} \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap (v \cup \{u\})))))$
30	20 29	bitrd	$⊢ \neg u \in ⋃ x \to (\forall z \in x (φ \to \exists! w w \in (z \cap v)) \leftrightarrow (\neg v \cup \{u\} \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap (v \cup \{u\})))))$
31		vex	$⊢ v \in V$
32		vsnex	$⊢ \{u\} \in V$
33	31 32	unex	$⊢ v \cup \{u\} \in V$
34		eleq1	$⊢ y = v \cup \{u\} \to (y \in x \leftrightarrow v \cup \{u\} \in x)$
35	34	notbid	$⊢ y = v \cup \{u\} \to (\neg y \in x \leftrightarrow \neg v \cup \{u\} \in x)$
36		ineq2	$⊢ y = v \cup \{u\} \to z \cap y = z \cap (v \cup \{u\})$
37	36	eleq2d	$⊢ y = v \cup \{u\} \to (w \in (z \cap y) \leftrightarrow w \in (z \cap (v \cup \{u\})))$
38	37	eubidv	$⊢ y = v \cup \{u\} \to (\exists! w w \in (z \cap y) \leftrightarrow \exists! w w \in (z \cap (v \cup \{u\})))$
39	38	imbi2d	$⊢ y = v \cup \{u\} \to ((φ \to \exists! w w \in (z \cap y)) \leftrightarrow (φ \to \exists! w w \in (z \cap (v \cup \{u\}))))$
40	39	ralbidv	$⊢ y = v \cup \{u\} \to (\forall z \in x (φ \to \exists! w w \in (z \cap y)) \leftrightarrow \forall z \in x (φ \to \exists! w w \in (z \cap (v \cup \{u\}))))$
41	35 40	anbi12d	$⊢ y = v \cup \{u\} \to ((\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y))) \leftrightarrow (\neg v \cup \{u\} \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap (v \cup \{u\})))))$
42	33 41	spcev	$⊢ (\neg v \cup \{u\} \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap (v \cup \{u\})))) \to \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y)))$
43	30 42	syl6bi	$⊢ \neg u \in ⋃ x \to (\forall z \in x (φ \to \exists! w w \in (z \cap v)) \to \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y))))$
44		vuniex	$⊢ ⋃ x \in V$
45		eleq2	$⊢ y = ⋃ x \to (u \in y \leftrightarrow u \in ⋃ x)$
46	45	notbid	$⊢ y = ⋃ x \to (\neg u \in y \leftrightarrow \neg u \in ⋃ x)$
47	46	exbidv	$⊢ y = ⋃ x \to (\exists u \neg u \in y \leftrightarrow \exists u \neg u \in ⋃ x)$
48		nalset	$⊢ \neg \exists y \forall u u \in y$
49		alexn	$⊢ \forall y \exists u \neg u \in y \leftrightarrow \neg \exists y \forall u u \in y$
50	48 49	mpbir	$⊢ \forall y \exists u \neg u \in y$
51	50	spi	$⊢ \exists u \neg u \in y$
52	44 47 51	vtocl	$⊢ \exists u \neg u \in ⋃ x$
53	43 52	exlimiiv	$⊢ \forall z \in x (φ \to \exists! w w \in (z \cap v)) \to \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y)))$
54	53	exlimiv	$⊢ \exists v \forall z \in x (φ \to \exists! w w \in (z \cap v)) \to \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y)))$
55	6 54	sylbi	$⊢ \exists y \forall z \in x (φ \to \exists! w w \in (z \cap y)) \to \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y)))$
56		exsimpr	$⊢ \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y))) \to \exists y \forall z \in x (φ \to \exists! w w \in (z \cap y))$
57	55 56	impbii	$⊢ \exists y \forall z \in x (φ \to \exists! w w \in (z \cap y)) \leftrightarrow \exists y (\neg y \in x \land \forall z \in x (φ \to \exists! w w \in (z \cap y)))$

Metamath Proof Explorer

Theorem kmlem2

Proof