This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑥 = 𝑧 → 𝐺 = 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 ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )