kmlem14

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

	Ref	Expression
Hypotheses	kmlem14.1	$⊢ φ \leftrightarrow (z \in y \to ((v \in x \land y \neq v) \land z \in v))$
	kmlem14.2	$⊢ ψ \leftrightarrow (z \in x \to ((v \in z \land v \in y) \land ((u \in z \land u \in y) \to u = v)))$
	kmlem14.3	$⊢ χ \leftrightarrow \forall z \in x \exists! v v \in (z \cap y)$
Assertion	kmlem14	$⊢ \exists z \in x \forall v \in z \exists w \in x (z \neq w \land v \in (z \cap w)) \leftrightarrow \exists y \forall z \exists v \forall u (y \in x \land φ)$

Proof

Step	Hyp	Ref	Expression
1		kmlem14.1	$⊢ φ \leftrightarrow (z \in y \to ((v \in x \land y \neq v) \land z \in v))$
2		kmlem14.2	$⊢ ψ \leftrightarrow (z \in x \to ((v \in z \land v \in y) \land ((u \in z \land u \in y) \to u = v)))$
3		kmlem14.3	$⊢ χ \leftrightarrow \forall z \in x \exists! v v \in (z \cap y)$
4		neeq1	$⊢ z = y \to (z \neq w \leftrightarrow y \neq w)$
5		ineq1	$⊢ z = y \to z \cap w = y \cap w$
6	5	eleq2d	$⊢ z = y \to (v \in (z \cap w) \leftrightarrow v \in (y \cap w))$
7	4 6	anbi12d	$⊢ z = y \to ((z \neq w \land v \in (z \cap w)) \leftrightarrow (y \neq w \land v \in (y \cap w)))$
8	7	rexbidv	$⊢ z = y \to (\exists w \in x (z \neq w \land v \in (z \cap w)) \leftrightarrow \exists w \in x (y \neq w \land v \in (y \cap w)))$
9	8	raleqbi1dv	$⊢ z = y \to (\forall v \in z \exists w \in x (z \neq w \land v \in (z \cap w)) \leftrightarrow \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w)))$
10	9	cbvrexvw	$⊢ \exists z \in x \forall v \in z \exists w \in x (z \neq w \land v \in (z \cap w)) \leftrightarrow \exists y \in x \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w))$
11		df-rex	$⊢ \exists y \in x \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w)) \leftrightarrow \exists y (y \in x \land \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w)))$
12		eleq1w	$⊢ v = z \to (v \in (y \cap w) \leftrightarrow z \in (y \cap w))$
13	12	anbi2d	$⊢ v = z \to ((y \neq w \land v \in (y \cap w)) \leftrightarrow (y \neq w \land z \in (y \cap w)))$
14	13	rexbidv	$⊢ v = z \to (\exists w \in x (y \neq w \land v \in (y \cap w)) \leftrightarrow \exists w \in x (y \neq w \land z \in (y \cap w)))$
15	14	cbvralvw	$⊢ \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w)) \leftrightarrow \forall z \in y \exists w \in x (y \neq w \land z \in (y \cap w))$
16		df-ral	$⊢ \forall z \in y \exists w \in x (y \neq w \land z \in (y \cap w)) \leftrightarrow \forall z (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w)))$
17	15 16	bitri	$⊢ \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w)) \leftrightarrow \forall z (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w)))$
18	17	anbi2i	$⊢ (y \in x \land \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w))) \leftrightarrow (y \in x \land \forall z (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w))))$
19		19.28v	$⊢ \forall z (y \in x \land (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w)))) \leftrightarrow (y \in x \land \forall z (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w))))$
20		neeq2	$⊢ w = v \to (y \neq w \leftrightarrow y \neq v)$
21		ineq2	$⊢ w = v \to y \cap w = y \cap v$
22	21	eleq2d	$⊢ w = v \to (z \in (y \cap w) \leftrightarrow z \in (y \cap v))$
23	20 22	anbi12d	$⊢ w = v \to ((y \neq w \land z \in (y \cap w)) \leftrightarrow (y \neq v \land z \in (y \cap v)))$
24	23	cbvrexvw	$⊢ \exists w \in x (y \neq w \land z \in (y \cap w)) \leftrightarrow \exists v \in x (y \neq v \land z \in (y \cap v))$
25		df-rex	$⊢ \exists v \in x (y \neq v \land z \in (y \cap v)) \leftrightarrow \exists v (v \in x \land (y \neq v \land z \in (y \cap v)))$
26	24 25	bitri	$⊢ \exists w \in x (y \neq w \land z \in (y \cap w)) \leftrightarrow \exists v (v \in x \land (y \neq v \land z \in (y \cap v)))$
27	26	imbi2i	$⊢ (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w))) \leftrightarrow (z \in y \to \exists v (v \in x \land (y \neq v \land z \in (y \cap v))))$
28		19.37v	$⊢ \exists v (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v)))) \leftrightarrow (z \in y \to \exists v (v \in x \land (y \neq v \land z \in (y \cap v))))$
29	27 28	bitr4i	$⊢ (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w))) \leftrightarrow \exists v (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v))))$
30	29	anbi2i	$⊢ (y \in x \land (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w)))) \leftrightarrow (y \in x \land \exists v (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v)))))$
31		19.42v	$⊢ \exists v (y \in x \land (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v))))) \leftrightarrow (y \in x \land \exists v (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v)))))$
32		19.3v	$⊢ \forall u (y \in x \land φ) \leftrightarrow (y \in x \land φ)$
33		elin	$⊢ z \in (y \cap v) \leftrightarrow (z \in y \land z \in v)$
34	33	baibr	$⊢ z \in y \to (z \in v \leftrightarrow z \in (y \cap v))$
35	34	anbi2d	$⊢ z \in y \to (((v \in x \land y \neq v) \land z \in v) \leftrightarrow ((v \in x \land y \neq v) \land z \in (y \cap v)))$
36		anass	$⊢ ((v \in x \land y \neq v) \land z \in (y \cap v)) \leftrightarrow (v \in x \land (y \neq v \land z \in (y \cap v)))$
37	35 36	bitrdi	$⊢ z \in y \to (((v \in x \land y \neq v) \land z \in v) \leftrightarrow (v \in x \land (y \neq v \land z \in (y \cap v))))$
38	37	pm5.74i	$⊢ (z \in y \to ((v \in x \land y \neq v) \land z \in v)) \leftrightarrow (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v))))$
39	1 38	bitri	$⊢ φ \leftrightarrow (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v))))$
40	39	anbi2i	$⊢ (y \in x \land φ) \leftrightarrow (y \in x \land (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v)))))$
41	32 40	bitr2i	$⊢ (y \in x \land (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v))))) \leftrightarrow \forall u (y \in x \land φ)$
42	41	exbii	$⊢ \exists v (y \in x \land (z \in y \to (v \in x \land (y \neq v \land z \in (y \cap v))))) \leftrightarrow \exists v \forall u (y \in x \land φ)$
43	30 31 42	3bitr2i	$⊢ (y \in x \land (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w)))) \leftrightarrow \exists v \forall u (y \in x \land φ)$
44	43	albii	$⊢ \forall z (y \in x \land (z \in y \to \exists w \in x (y \neq w \land z \in (y \cap w)))) \leftrightarrow \forall z \exists v \forall u (y \in x \land φ)$
45	18 19 44	3bitr2i	$⊢ (y \in x \land \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w))) \leftrightarrow \forall z \exists v \forall u (y \in x \land φ)$
46	45	exbii	$⊢ \exists y (y \in x \land \forall v \in y \exists w \in x (y \neq w \land v \in (y \cap w))) \leftrightarrow \exists y \forall z \exists v \forall u (y \in x \land φ)$
47	10 11 46	3bitri	$⊢ \exists z \in x \forall v \in z \exists w \in x (z \neq w \land v \in (z \cap w)) \leftrightarrow \exists y \forall z \exists v \forall u (y \in x \land φ)$

Metamath Proof Explorer

Theorem kmlem14

Proof