Theorem unxpdomlem2

Description: Lemma for unxpdom . (Contributed by Mario Carneiro, 13-Jan-2013)

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

Proof

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