Theorem unxpdomlem1

Description: Lemma for unxpdom . (Trivial substitution proof.) (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)$$
Assertion	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)$$

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		elequ1	$$⊢x=z\to \left(x\in a\leftrightarrow z\in a\right)$$
4		opeq1	$$⊢x=z\to ⟨x,if\left(x=m,t,s\right)⟩=⟨z,if\left(x=m,t,s\right)⟩$$
5		equequ1	$$⊢x=z\to \left(x=m\leftrightarrow z=m\right)$$
6	5	ifbid	$$⊢x=z\to if\left(x=m,t,s\right)=if\left(z=m,t,s\right)$$
7	6	opeq2d	$$⊢x=z\to ⟨z,if\left(x=m,t,s\right)⟩=⟨z,if\left(z=m,t,s\right)⟩$$
8	4 7	eqtrd	$$⊢x=z\to ⟨x,if\left(x=m,t,s\right)⟩=⟨z,if\left(z=m,t,s\right)⟩$$
9		equequ1	$$⊢x=z\to \left(x=t\leftrightarrow z=t\right)$$
10	9	ifbid	$$⊢x=z\to if\left(x=t,n,m\right)=if\left(z=t,n,m\right)$$
11	10	opeq1d	$$⊢x=z\to ⟨if\left(x=t,n,m\right),x⟩=⟨if\left(z=t,n,m\right),x⟩$$
12		opeq2	$$⊢x=z\to ⟨if\left(z=t,n,m\right),x⟩=⟨if\left(z=t,n,m\right),z⟩$$
13	11 12	eqtrd	$$⊢x=z\to ⟨if\left(x=t,n,m\right),x⟩=⟨if\left(z=t,n,m\right),z⟩$$
14	3 8 13	ifbieq12d	$$⊢x=z\to if\left(x\in a,⟨x,if\left(x=m,t,s\right)⟩,⟨if\left(x=t,n,m\right),x⟩\right)=if\left(z\in a,⟨z,if\left(z=m,t,s\right)⟩,⟨if\left(z=t,n,m\right),z⟩\right)$$
15	2 14	eqtrid	$$⊢x=z\to G=if\left(z\in a,⟨z,if\left(z=m,t,s\right)⟩,⟨if\left(z=t,n,m\right),z⟩\right)$$
16		opex	$$⊢⟨z,if\left(z=m,t,s\right)⟩\in \mathrm{V}$$
17		opex	$$⊢⟨if\left(z=t,n,m\right),z⟩\in \mathrm{V}$$
18	16 17	ifex	$$⊢if\left(z\in a,⟨z,if\left(z=m,t,s\right)⟩,⟨if\left(z=t,n,m\right),z⟩\right)\in \mathrm{V}$$
19	15 1 18	fvmpt	$$⊢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)$$