unxpdomlem2

	Ref	Expression
Hypotheses	unxpdomlem1.1	$⊢ F = (x \in (a \cup b) ⟼ G)$
	unxpdomlem1.2	$⊢ G = if (x \in a, ⟨x, if (x = m, t, s)⟩, ⟨if (x = t, n, m), x⟩)$
	unxpdomlem2.1	$⊢ φ \to w \in (a \cup b)$
	unxpdomlem2.2	$⊢ φ \to \neg m = n$
	unxpdomlem2.3	$⊢ φ \to \neg s = t$
Assertion	unxpdomlem2	$⊢ (φ \land (z \in a \land \neg w \in a)) \to \neg F (z) = F (w)$

Proof

Step	Hyp	Ref	Expression
1		unxpdomlem1.1	$⊢ F = (x \in (a \cup b) ⟼ G)$
2		unxpdomlem1.2	$⊢ G = if (x \in a, ⟨x, if (x = m, t, s)⟩, ⟨if (x = t, n, m), x⟩)$
3		unxpdomlem2.1	$⊢ φ \to w \in (a \cup b)$
4		unxpdomlem2.2	$⊢ φ \to \neg m = n$
5		unxpdomlem2.3	$⊢ φ \to \neg s = t$
6	5	adantr	$⊢ (φ \land (z \in a \land \neg w \in a)) \to \neg s = t$
7		elun1	$⊢ z \in a \to z \in (a \cup b)$
8	7	ad2antrl	$⊢ (φ \land (z \in a \land \neg w \in a)) \to z \in (a \cup b)$
9	1 2	unxpdomlem1	$⊢ z \in (a \cup b) \to F (z) = if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩)$
10	8 9	syl	$⊢ (φ \land (z \in a \land \neg w \in a)) \to F (z) = if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩)$
11		iftrue	$⊢ z \in a \to if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩) = ⟨z, if (z = m, t, s)⟩$
12	11	ad2antrl	$⊢ (φ \land (z \in a \land \neg w \in a)) \to if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩) = ⟨z, if (z = m, t, s)⟩$
13	10 12	eqtrd	$⊢ (φ \land (z \in a \land \neg w \in a)) \to F (z) = ⟨z, if (z = m, t, s)⟩$
14	3	adantr	$⊢ (φ \land (z \in a \land \neg w \in a)) \to w \in (a \cup b)$
15	1 2	unxpdomlem1	$⊢ w \in (a \cup b) \to F (w) = if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩)$
16	14 15	syl	$⊢ (φ \land (z \in a \land \neg w \in a)) \to F (w) = if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩)$
17		iffalse	$⊢ \neg w \in a \to if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩) = ⟨if (w = t, n, m), w⟩$
18	17	ad2antll	$⊢ (φ \land (z \in a \land \neg w \in a)) \to if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩) = ⟨if (w = t, n, m), w⟩$
19	16 18	eqtrd	$⊢ (φ \land (z \in a \land \neg w \in a)) \to F (w) = ⟨if (w = t, n, m), w⟩$
20	13 19	eqeq12d	$⊢ (φ \land (z \in a \land \neg w \in a)) \to (F (z) = F (w) \leftrightarrow ⟨z, if (z = m, t, s)⟩ = ⟨if (w = t, n, m), w⟩)$
21	20	biimpa	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to ⟨z, if (z = m, t, s)⟩ = ⟨if (w = t, n, m), w⟩$
22		vex	$⊢ z \in V$
23		vex	$⊢ t \in V$
24		vex	$⊢ s \in V$
25	23 24	ifex	$⊢ if (z = m, t, s) \in V$
26	22 25	opth	$⊢ ⟨z, if (z = m, t, s)⟩ = ⟨if (w = t, n, m), w⟩ \leftrightarrow (z = if (w = t, n, m) \land if (z = m, t, s) = w)$
27	21 26	sylib	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (z = if (w = t, n, m) \land if (z = m, t, s) = w)$
28	27	simprd	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to if (z = m, t, s) = w$
29		iftrue	$⊢ z = m \to if (z = m, t, s) = t$
30	28	eqeq1d	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (if (z = m, t, s) = t \leftrightarrow w = t)$
31	29 30	imbitrid	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (z = m \to w = t)$
32		iftrue	$⊢ w = t \to if (w = t, n, m) = n$
33	27	simpld	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to z = if (w = t, n, m)$
34	33	eqeq1d	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (z = n \leftrightarrow if (w = t, n, m) = n)$
35	32 34	imbitrrid	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (w = t \to z = n)$
36	31 35	syld	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (z = m \to z = n)$
37	4	ad2antrr	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to \neg m = n$
38		equequ1	$⊢ z = m \to (z = n \leftrightarrow m = n)$
39	38	notbid	$⊢ z = m \to (\neg z = n \leftrightarrow \neg m = n)$
40	37 39	syl5ibrcom	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (z = m \to \neg z = n)$
41	36 40	pm2.65d	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to \neg z = m$
42	41	iffalsed	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to if (z = m, t, s) = s$
43		iffalse	$⊢ \neg w = t \to if (w = t, n, m) = m$
44	33	eqeq1d	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (z = m \leftrightarrow if (w = t, n, m) = m)$
45	43 44	imbitrrid	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to (\neg w = t \to z = m)$
46	41 45	mt3d	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to w = t$
47	28 42 46	3eqtr3d	$⊢ ((φ \land (z \in a \land \neg w \in a)) \land F (z) = F (w)) \to s = t$
48	6 47	mtand	$⊢ (φ \land (z \in a \land \neg w \in a)) \to \neg F (z) = F (w)$

Metamath Proof Explorer

Theorem unxpdomlem2

Proof