Theorem unxpdomlem1

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

	Ref	Expression
Hypotheses	unxpdomlem1.1	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ↦ 𝐺 )
	unxpdomlem1.2	⊢ 𝐺 = if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ )
Assertion	unxpdomlem1	⊢ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		unxpdomlem1.1	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ↦ 𝐺 )
2		unxpdomlem1.2	⊢ 𝐺 = if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ )
3		elequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑎 ↔ 𝑧 ∈ 𝑎 ) )
4		opeq1	⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ 𝑧 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
5		equequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑚 ↔ 𝑧 = 𝑚 ) )
6	5	ifbid	⊢ ( 𝑥 = 𝑧 → if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) = if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) )
7	6	opeq2d	⊢ ( 𝑥 = 𝑧 → ⟨ 𝑧 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
8	4 7	eqtrd	⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
9		equequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑡 ↔ 𝑧 = 𝑡 ) )
10	9	ifbid	⊢ ( 𝑥 = 𝑧 → if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) = if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) )
11	10	opeq1d	⊢ ( 𝑥 = 𝑧 → ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ )
12		opeq2	⊢ ( 𝑥 = 𝑧 → ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
13	11 12	eqtrd	⊢ ( 𝑥 = 𝑧 → ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ = ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ )
14	3 8 13	ifbieq12d	⊢ ( 𝑥 = 𝑧 → if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
15	2 14	syl5eq	⊢ ( 𝑥 = 𝑧 → 𝐺 = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
16		opex	⊢ ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ ∈ V
17		opex	⊢ ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ∈ V
18	16 17	ifex	⊢ if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) ∈ V
19	15 1 18	fvmpt	⊢ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )