unirep

Description: Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011)

	Ref	Expression
Hypotheses	unirep.1	$⊢ y = D \to (φ \leftrightarrow ψ)$
	unirep.2	$⊢ y = D \to B = C$
	unirep.3	$⊢ y = z \to (φ \leftrightarrow χ)$
	unirep.4	$⊢ y = z \to B = F$
	unirep.5	$⊢ B \in V$
Assertion	unirep	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to (ι x \| \exists y \in A (φ \land x = B)) = C$

Proof

Step	Hyp	Ref	Expression
1		unirep.1	$⊢ y = D \to (φ \leftrightarrow ψ)$
2		unirep.2	$⊢ y = D \to B = C$
3		unirep.3	$⊢ y = z \to (φ \leftrightarrow χ)$
4		unirep.4	$⊢ y = z \to B = F$
5		unirep.5	$⊢ B \in V$
6		eqidd	$⊢ ψ \to C = C$
7	6	ancli	$⊢ ψ \to (ψ \land C = C)$
8	2	eqeq2d	$⊢ y = D \to (C = B \leftrightarrow C = C)$
9	1 8	anbi12d	$⊢ y = D \to ((φ \land C = B) \leftrightarrow (ψ \land C = C))$
10	9	rspcev	$⊢ (D \in A \land (ψ \land C = C)) \to \exists y \in A (φ \land C = B)$
11	7 10	sylan2	$⊢ (D \in A \land ψ) \to \exists y \in A (φ \land C = B)$
12	11	adantl	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to \exists y \in A (φ \land C = B)$
13		nfcvd	$⊢ D \in A \to \underline{Ⅎ} y C$
14	13 2	csbiegf	$⊢ D \in A \to ⦋ D / y ⦌ B = C$
15	5	csbex	$⊢ ⦋ D / y ⦌ B \in V$
16	14 15	eqeltrrdi	$⊢ D \in A \to C \in V$
17	16	ad2antrl	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to C \in V$
18		eqeq1	$⊢ x = C \to (x = B \leftrightarrow C = B)$
19	18	anbi2d	$⊢ x = C \to ((φ \land x = B) \leftrightarrow (φ \land C = B))$
20	19	rexbidv	$⊢ x = C \to (\exists y \in A (φ \land x = B) \leftrightarrow \exists y \in A (φ \land C = B))$
21	20	spcegv	$⊢ C \in V \to (\exists y \in A (φ \land C = B) \to \exists x \exists y \in A (φ \land x = B))$
22	16 21	syl	$⊢ D \in A \to (\exists y \in A (φ \land C = B) \to \exists x \exists y \in A (φ \land x = B))$
23	22	adantr	$⊢ (D \in A \land ψ) \to (\exists y \in A (φ \land C = B) \to \exists x \exists y \in A (φ \land x = B))$
24	11 23	mpd	$⊢ (D \in A \land ψ) \to \exists x \exists y \in A (φ \land x = B)$
25	24	adantl	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to \exists x \exists y \in A (φ \land x = B)$
26		r19.29	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land \exists y \in A (φ \land x = B)) \to \exists y \in A (\forall z \in A ((φ \land χ) \to B = F) \land (φ \land x = B))$
27		r19.29	$⊢ (\forall z \in A ((φ \land χ) \to B = F) \land \exists z \in A (χ \land w = F)) \to \exists z \in A (((φ \land χ) \to B = F) \land (χ \land w = F))$
28		an4	$⊢ ((φ \land x = B) \land (χ \land w = F)) \leftrightarrow ((φ \land χ) \land (x = B \land w = F))$
29		pm3.35	$⊢ ((φ \land χ) \land ((φ \land χ) \to B = F)) \to B = F$
30		eqeq12	$⊢ (x = B \land w = F) \to (x = w \leftrightarrow B = F)$
31	29 30	syl5ibrcom	$⊢ ((φ \land χ) \land ((φ \land χ) \to B = F)) \to ((x = B \land w = F) \to x = w)$
32	31	ancoms	$⊢ (((φ \land χ) \to B = F) \land (φ \land χ)) \to ((x = B \land w = F) \to x = w)$
33	32	expimpd	$⊢ ((φ \land χ) \to B = F) \to (((φ \land χ) \land (x = B \land w = F)) \to x = w)$
34	28 33	biimtrid	$⊢ ((φ \land χ) \to B = F) \to (((φ \land x = B) \land (χ \land w = F)) \to x = w)$
35	34	ancomsd	$⊢ ((φ \land χ) \to B = F) \to (((χ \land w = F) \land (φ \land x = B)) \to x = w)$
36	35	expdimp	$⊢ (((φ \land χ) \to B = F) \land (χ \land w = F)) \to ((φ \land x = B) \to x = w)$
37	36	rexlimivw	$⊢ \exists z \in A (((φ \land χ) \to B = F) \land (χ \land w = F)) \to ((φ \land x = B) \to x = w)$
38	37	imp	$⊢ (\exists z \in A (((φ \land χ) \to B = F) \land (χ \land w = F)) \land (φ \land x = B)) \to x = w$
39	27 38	sylan	$⊢ ((\forall z \in A ((φ \land χ) \to B = F) \land \exists z \in A (χ \land w = F)) \land (φ \land x = B)) \to x = w$
40	39	an32s	$⊢ ((\forall z \in A ((φ \land χ) \to B = F) \land (φ \land x = B)) \land \exists z \in A (χ \land w = F)) \to x = w$
41	40	ex	$⊢ (\forall z \in A ((φ \land χ) \to B = F) \land (φ \land x = B)) \to (\exists z \in A (χ \land w = F) \to x = w)$
42	41	rexlimivw	$⊢ \exists y \in A (\forall z \in A ((φ \land χ) \to B = F) \land (φ \land x = B)) \to (\exists z \in A (χ \land w = F) \to x = w)$
43	26 42	syl	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land \exists y \in A (φ \land x = B)) \to (\exists z \in A (χ \land w = F) \to x = w)$
44	43	expimpd	$⊢ \forall y \in A \forall z \in A ((φ \land χ) \to B = F) \to ((\exists y \in A (φ \land x = B) \land \exists z \in A (χ \land w = F)) \to x = w)$
45	44	adantr	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to ((\exists y \in A (φ \land x = B) \land \exists z \in A (χ \land w = F)) \to x = w)$
46	45	alrimivv	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to \forall x \forall w ((\exists y \in A (φ \land x = B) \land \exists z \in A (χ \land w = F)) \to x = w)$
47		eqeq1	$⊢ x = w \to (x = B \leftrightarrow w = B)$
48	47	anbi2d	$⊢ x = w \to ((φ \land x = B) \leftrightarrow (φ \land w = B))$
49	48	rexbidv	$⊢ x = w \to (\exists y \in A (φ \land x = B) \leftrightarrow \exists y \in A (φ \land w = B))$
50	4	eqeq2d	$⊢ y = z \to (w = B \leftrightarrow w = F)$
51	3 50	anbi12d	$⊢ y = z \to ((φ \land w = B) \leftrightarrow (χ \land w = F))$
52	51	cbvrexvw	$⊢ \exists y \in A (φ \land w = B) \leftrightarrow \exists z \in A (χ \land w = F)$
53	49 52	bitrdi	$⊢ x = w \to (\exists y \in A (φ \land x = B) \leftrightarrow \exists z \in A (χ \land w = F))$
54	53	eu4	$⊢ \exists! x \exists y \in A (φ \land x = B) \leftrightarrow (\exists x \exists y \in A (φ \land x = B) \land \forall x \forall w ((\exists y \in A (φ \land x = B) \land \exists z \in A (χ \land w = F)) \to x = w))$
55	25 46 54	sylanbrc	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to \exists! x \exists y \in A (φ \land x = B)$
56	20	iota2	$⊢ (C \in V \land \exists! x \exists y \in A (φ \land x = B)) \to (\exists y \in A (φ \land C = B) \leftrightarrow (ι x \| \exists y \in A (φ \land x = B)) = C)$
57	17 55 56	syl2anc	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to (\exists y \in A (φ \land C = B) \leftrightarrow (ι x \| \exists y \in A (φ \land x = B)) = C)$
58	12 57	mpbid	$⊢ (\forall y \in A \forall z \in A ((φ \land χ) \to B = F) \land (D \in A \land ψ)) \to (ι x \| \exists y \in A (φ \land x = B)) = C$

Metamath Proof Explorer

Theorem unirep

Proof