Metamath Proof Explorer


Theorem unxpdomlem3

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

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
Assertion unxpdomlem3 1 𝑜 a 1 𝑜 b a b a × b

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 1sdom a V 1 𝑜 a m a n a ¬ m = n
4 3 elv 1 𝑜 a m a n a ¬ m = n
5 1sdom b V 1 𝑜 b s b t b ¬ s = t
6 5 elv 1 𝑜 b s b t b ¬ s = t
7 reeanv m a s b n a ¬ m = n t b ¬ s = t m a n a ¬ m = n s b t b ¬ s = t
8 reeanv n a t b ¬ m = n ¬ s = t n a ¬ m = n t b ¬ s = t
9 vex a V
10 vex b V
11 9 10 unex a b V
12 9 10 xpex a × b V
13 simpr m a s b n a t b ¬ m = n ¬ s = t x a b x a x a
14 simp2r m a s b n a t b ¬ m = n ¬ s = t t b
15 simp1r m a s b n a t b ¬ m = n ¬ s = t s b
16 14 15 ifcld m a s b n a t b ¬ m = n ¬ s = t if x = m t s b
17 16 ad2antrr m a s b n a t b ¬ m = n ¬ s = t x a b x a if x = m t s b
18 13 17 opelxpd m a s b n a t b ¬ m = n ¬ s = t x a b x a x if x = m t s a × b
19 simp2l m a s b n a t b ¬ m = n ¬ s = t n a
20 simp1l m a s b n a t b ¬ m = n ¬ s = t m a
21 19 20 ifcld m a s b n a t b ¬ m = n ¬ s = t if x = t n m a
22 21 ad2antrr m a s b n a t b ¬ m = n ¬ s = t x a b ¬ x a if x = t n m a
23 simpr m a s b n a t b ¬ m = n ¬ s = t x a b x a b
24 elun x a b x a x b
25 23 24 sylib m a s b n a t b ¬ m = n ¬ s = t x a b x a x b
26 25 orcanai m a s b n a t b ¬ m = n ¬ s = t x a b ¬ x a x b
27 22 26 opelxpd m a s b n a t b ¬ m = n ¬ s = t x a b ¬ x a if x = t n m x a × b
28 18 27 ifclda m a s b n a t b ¬ m = n ¬ s = t x a b if x a x if x = m t s if x = t n m x a × b
29 2 28 eqeltrid m a s b n a t b ¬ m = n ¬ s = t x a b G a × b
30 29 1 fmptd m a s b n a t b ¬ m = n ¬ s = t F : a b a × b
31 1 2 unxpdomlem1 z a b F z = if z a z if z = m t s if z = t n m z
32 31 ad2antrl ¬ m = n ¬ s = t z a b w a b F z = if z a z if z = m t s if z = t n m z
33 iftrue z a if z a z if z = m t s if z = t n m z = z if z = m t s
34 33 adantr 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
35 32 34 sylan9eq ¬ m = n ¬ s = t z a b w a b z a w a F z = z if z = m t s
36 1 2 unxpdomlem1 w a b F w = if w a w if w = m t s if w = t n m w
37 36 ad2antll ¬ m = n ¬ s = t z a b w a b F w = if w a w if w = m t s if w = t n m w
38 iftrue w a if w a w if w = m t s if w = t n m w = w if w = m t s
39 38 adantl z a w a if w a w if w = m t s if w = t n m w = w if w = m t s
40 37 39 sylan9eq ¬ m = n ¬ s = t z a b w a b z a w a F w = w if w = m t s
41 35 40 eqeq12d ¬ m = n ¬ s = t z a b w a b z a w a F z = F w z if z = m t s = w if w = m t s
42 vex z V
43 vex t V
44 vex s V
45 43 44 ifex if z = m t s V
46 42 45 opth1 z if z = m t s = w if w = m t s z = w
47 41 46 syl6bi ¬ m = n ¬ s = t z a b w a b z a w a F z = F w z = w
48 simprr ¬ m = n ¬ s = t z a b w a b w a b
49 simpll ¬ m = n ¬ s = t z a b w a b ¬ m = n
50 simplr ¬ m = n ¬ s = t z a b w a b ¬ s = t
51 1 2 48 49 50 unxpdomlem2 ¬ m = n ¬ s = t z a b w a b z a ¬ w a ¬ F z = F w
52 51 pm2.21d ¬ m = n ¬ s = t z a b w a b z a ¬ w a F z = F w z = w
53 eqcom F z = F w F w = F z
54 simprl ¬ m = n ¬ s = t z a b w a b z a b
55 1 2 54 49 50 unxpdomlem2 ¬ m = n ¬ s = t z a b w a b w a ¬ z a ¬ F w = F z
56 55 ancom2s ¬ m = n ¬ s = t z a b w a b ¬ z a w a ¬ F w = F z
57 56 pm2.21d ¬ m = n ¬ s = t z a b w a b ¬ z a w a F w = F z z = w
58 53 57 syl5bi ¬ m = n ¬ s = t z a b w a b ¬ z a w a F z = F w z = w
59 iffalse ¬ z a if z a z if z = m t s if z = t n m z = if z = t n m z
60 59 adantr ¬ z a ¬ w a if z a z if z = m t s if z = t n m z = if z = t n m z
61 32 60 sylan9eq ¬ m = n ¬ s = t z a b w a b ¬ z a ¬ w a F z = if z = t n m z
62 iffalse ¬ w a if w a w if w = m t s if w = t n m w = if w = t n m w
63 62 adantl ¬ 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
64 37 63 sylan9eq ¬ m = n ¬ s = t z a b w a b ¬ z a ¬ w a F w = if w = t n m w
65 61 64 eqeq12d ¬ m = n ¬ s = t z a b w a b ¬ z a ¬ w a F z = F w if z = t n m z = if w = t n m w
66 vex n V
67 vex m V
68 66 67 ifex if z = t n m V
69 68 42 opth if z = t n m z = if w = t n m w if z = t n m = if w = t n m z = w
70 69 simprbi if z = t n m z = if w = t n m w z = w
71 65 70 syl6bi ¬ m = n ¬ s = t z a b w a b ¬ z a ¬ w a F z = F w z = w
72 47 52 58 71 4casesdan ¬ m = n ¬ s = t z a b w a b F z = F w z = w
73 72 ralrimivva ¬ m = n ¬ s = t z a b w a b F z = F w z = w
74 73 3ad2ant3 m a s b n a t b ¬ m = n ¬ s = t z a b w a b F z = F w z = w
75 dff13 F : a b 1-1 a × b F : a b a × b z a b w a b F z = F w z = w
76 30 74 75 sylanbrc m a s b n a t b ¬ m = n ¬ s = t F : a b 1-1 a × b
77 f1dom2g a b V a × b V F : a b 1-1 a × b a b a × b
78 11 12 76 77 mp3an12i m a s b n a t b ¬ m = n ¬ s = t a b a × b
79 78 3expia m a s b n a t b ¬ m = n ¬ s = t a b a × b
80 79 rexlimdvva m a s b n a t b ¬ m = n ¬ s = t a b a × b
81 8 80 syl5bir m a s b n a ¬ m = n t b ¬ s = t a b a × b
82 81 rexlimivv m a s b n a ¬ m = n t b ¬ s = t a b a × b
83 7 82 sylbir m a n a ¬ m = n s b t b ¬ s = t a b a × b
84 4 6 83 syl2anb 1 𝑜 a 1 𝑜 b a b a × b