Metamath Proof Explorer


Theorem unxpdomlem2

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

Ref Expression
Hypotheses unxpdomlem1.1 F = x a b G
unxpdomlem1.2 G = if x a x if x = m t s if x = t n m x
unxpdomlem2.1 φ w a b
unxpdomlem2.2 φ ¬ m = n
unxpdomlem2.3 φ ¬ s = t
Assertion unxpdomlem2 φ z a ¬ w a ¬ F z = F w

Proof

Step Hyp Ref Expression
1 unxpdomlem1.1 F = x a b G
2 unxpdomlem1.2 G = if x a x if x = m t s if x = t n m x
3 unxpdomlem2.1 φ w a b
4 unxpdomlem2.2 φ ¬ m = n
5 unxpdomlem2.3 φ ¬ s = t
6 5 adantr φ z a ¬ w a ¬ s = t
7 elun1 z a z a b
8 7 ad2antrl φ z a ¬ w a z a b
9 1 2 unxpdomlem1 z a b F z = if z a z if z = m t s if z = t n m z
10 8 9 syl φ z a ¬ w a F z = if z a z if z = m t s if z = t n m z
11 iftrue z a if z a z if z = m t s if z = t n m z = z if z = m t s
12 11 ad2antrl φ z a ¬ w a if z a z if z = m t s if z = t n m z = z if z = m t s
13 10 12 eqtrd φ z a ¬ w a F z = z if z = m t s
14 3 adantr φ z a ¬ w a w a b
15 1 2 unxpdomlem1 w a b F w = if w a w if w = m t s if w = t n m w
16 14 15 syl φ z a ¬ w a F w = if w a w if w = m t s if w = t n m w
17 iffalse ¬ w a if w a w if w = m t s if w = t n m w = if w = t n m w
18 17 ad2antll φ z a ¬ w a if w a w if w = m t s if w = t n m w = if w = t n m w
19 16 18 eqtrd φ z a ¬ w a F w = if w = t n m w
20 13 19 eqeq12d φ z a ¬ w a F z = F w z if z = m t s = if w = t n m w
21 20 biimpa φ z a ¬ w a F z = F w z if z = m t s = if w = t n m w
22 vex z V
23 vex t V
24 vex s V
25 23 24 ifex if z = m t s V
26 22 25 opth z if z = m t s = if w = t n m w z = if w = t n m if z = m t s = w
27 21 26 sylib φ z a ¬ w a F z = F w z = if w = t n m if z = m t s = w
28 27 simprd φ z a ¬ w a F z = F w if z = m t s = w
29 iftrue z = m if z = m t s = t
30 28 eqeq1d φ z a ¬ w a F z = F w if z = m t s = t w = t
31 29 30 syl5ib φ z a ¬ w a F z = F w z = m w = t
32 iftrue w = t if w = t n m = n
33 27 simpld φ z a ¬ w a F z = F w z = if w = t n m
34 33 eqeq1d φ z a ¬ w a F z = F w z = n if w = t n m = n
35 32 34 syl5ibr φ z a ¬ w a F z = F w w = t z = n
36 31 35 syld φ z a ¬ w a F z = F w z = m z = n
37 4 ad2antrr φ z a ¬ w a F z = F w ¬ m = n
38 equequ1 z = m z = n m = n
39 38 notbid z = m ¬ z = n ¬ m = n
40 37 39 syl5ibrcom φ z a ¬ w a F z = F w z = m ¬ z = n
41 36 40 pm2.65d φ z a ¬ w a F z = F w ¬ z = m
42 41 iffalsed φ z a ¬ w a F z = F w if z = m t s = s
43 iffalse ¬ w = t if w = t n m = m
44 33 eqeq1d φ z a ¬ w a F z = F w z = m if w = t n m = m
45 43 44 syl5ibr φ z a ¬ w a F z = F w ¬ w = t z = m
46 41 45 mt3d φ z a ¬ w a F z = F w w = t
47 28 42 46 3eqtr3d φ z a ¬ w a F z = F w s = t
48 6 47 mtand φ z a ¬ w a ¬ F z = F w