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

Metamath Proof Explorer

Theorem unxpdomlem2

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

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

Proof

Step Hyp Ref Expression
1 unxpdomlem1.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑎 ∪ 𝑏 ) ↦ 𝐺 )
2 unxpdomlem1.2 ⊢ 𝐺 = if ( 𝑥 ∈ 𝑎 , ⟨ 𝑥 , if ( 𝑥 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑥 = 𝑡 , 𝑛 , 𝑚 ) , 𝑥 ⟩ )
3 unxpdomlem2.1 ⊢ ( 𝜑 → 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) )
4 unxpdomlem2.2 ⊢ ( 𝜑 → ¬ 𝑚 = 𝑛 )
5 unxpdomlem2.3 ⊢ ( 𝜑 → ¬ 𝑠 = 𝑡 )
6 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ¬ 𝑠 = 𝑡 )
7 elun1 ⊢ ( 𝑧 ∈ 𝑎 → 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) )
8 7 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) )
9 1 2 unxpdomlem1 ⊢ ( 𝑧 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
10 8 9 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) )
11 iftrue ⊢ ( 𝑧 ∈ 𝑎 → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
12 11 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → if ( 𝑧 ∈ 𝑎 , ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑧 = 𝑡 , 𝑛 , 𝑚 ) , 𝑧 ⟩ ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
13 10 12 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑧 ) = ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ )
14 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) )
15 1 2 unxpdomlem1 ⊢ ( 𝑤 ∈ ( 𝑎 ∪ 𝑏 ) → ( 𝐹 ‘ 𝑤 ) = if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
16 14 15 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑤 ) = if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
17 iffalse ⊢ ( ¬ 𝑤 ∈ 𝑎 → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
18 17 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → if ( 𝑤 ∈ 𝑎 , ⟨ 𝑤 , if ( 𝑤 = 𝑚 , 𝑡 , 𝑠 ) ⟩ , ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
19 16 18 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( 𝐹 ‘ 𝑤 ) = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
20 13 19 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ) )
21 20 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ )
22 vex ⊢ 𝑧 ∈ V
23 vex ⊢ 𝑡 ∈ V
24 vex ⊢ 𝑠 ∈ V
25 23 24 ifex ⊢ if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ∈ V
26 22 25 opth ⊢ ( ⟨ 𝑧 , if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) ⟩ = ⟨ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) , 𝑤 ⟩ ↔ ( 𝑧 = if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) ∧ if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) = 𝑤 ) )
27 21 26 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 = if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) ∧ if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) = 𝑤 ) )
28 27 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) = 𝑤 )
29 iftrue ⊢ ( 𝑧 = 𝑚 → if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) = 𝑡 )
30 28 eqeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) = 𝑡 ↔ 𝑤 = 𝑡 ) )
31 29 30 imbitrid ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 = 𝑚 → 𝑤 = 𝑡 ) )
32 iftrue ⊢ ( 𝑤 = 𝑡 → if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) = 𝑛 )
33 27 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑧 = if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) )
34 33 eqeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 = 𝑛 ↔ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) = 𝑛 ) )
35 32 34 imbitrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑤 = 𝑡 → 𝑧 = 𝑛 ) )
36 31 35 syld ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 = 𝑚 → 𝑧 = 𝑛 ) )
37 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ¬ 𝑚 = 𝑛 )
38 equequ1 ⊢ ( 𝑧 = 𝑚 → ( 𝑧 = 𝑛 ↔ 𝑚 = 𝑛 ) )
39 38 notbid ⊢ ( 𝑧 = 𝑚 → ( ¬ 𝑧 = 𝑛 ↔ ¬ 𝑚 = 𝑛 ) )
40 37 39 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 = 𝑚 → ¬ 𝑧 = 𝑛 ) )
41 36 40 pm2.65d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ¬ 𝑧 = 𝑚 )
42 41 iffalsed ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → if ( 𝑧 = 𝑚 , 𝑡 , 𝑠 ) = 𝑠 )
43 iffalse ⊢ ( ¬ 𝑤 = 𝑡 → if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) = 𝑚 )
44 33 eqeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 = 𝑚 ↔ if ( 𝑤 = 𝑡 , 𝑛 , 𝑚 ) = 𝑚 ) )
45 43 44 imbitrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( ¬ 𝑤 = 𝑡 → 𝑧 = 𝑚 ) )
46 41 45 mt3d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑤 = 𝑡 )
47 28 42 46 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑠 = 𝑡 )
48 6 47 mtand ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎 ) ) → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )