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=xabG
unxpdomlem1.2 G=ifxaxifx=mtsifx=tnmx
Assertion unxpdomlem3 1𝑜a1𝑜baba×b

Proof

Step Hyp Ref Expression
1 unxpdomlem1.1 F=xabG
2 unxpdomlem1.2 G=ifxaxifx=mtsifx=tnmx
3 1sdom aV1𝑜amana¬m=n
4 3 elv 1𝑜amana¬m=n
5 1sdom bV1𝑜bsbtb¬s=t
6 5 elv 1𝑜bsbtb¬s=t
7 reeanv masbna¬m=ntb¬s=tmana¬m=nsbtb¬s=t
8 reeanv natb¬m=n¬s=tna¬m=ntb¬s=t
9 vex aV
10 vex bV
11 9 10 unex abV
12 9 10 xpex a×bV
13 simpr masbnatb¬m=n¬s=txabxaxa
14 simp2r masbnatb¬m=n¬s=ttb
15 simp1r masbnatb¬m=n¬s=tsb
16 14 15 ifcld masbnatb¬m=n¬s=tifx=mtsb
17 16 ad2antrr masbnatb¬m=n¬s=txabxaifx=mtsb
18 13 17 opelxpd masbnatb¬m=n¬s=txabxaxifx=mtsa×b
19 simp2l masbnatb¬m=n¬s=tna
20 simp1l masbnatb¬m=n¬s=tma
21 19 20 ifcld masbnatb¬m=n¬s=tifx=tnma
22 21 ad2antrr masbnatb¬m=n¬s=txab¬xaifx=tnma
23 simpr masbnatb¬m=n¬s=txabxab
24 elun xabxaxb
25 23 24 sylib masbnatb¬m=n¬s=txabxaxb
26 25 orcanai masbnatb¬m=n¬s=txab¬xaxb
27 22 26 opelxpd masbnatb¬m=n¬s=txab¬xaifx=tnmxa×b
28 18 27 ifclda masbnatb¬m=n¬s=txabifxaxifx=mtsifx=tnmxa×b
29 2 28 eqeltrid masbnatb¬m=n¬s=txabGa×b
30 29 1 fmptd masbnatb¬m=n¬s=tF:aba×b
31 1 2 unxpdomlem1 zabFz=ifzazifz=mtsifz=tnmz
32 31 ad2antrl ¬m=n¬s=tzabwabFz=ifzazifz=mtsifz=tnmz
33 iftrue zaifzazifz=mtsifz=tnmz=zifz=mts
34 33 adantr zawaifzazifz=mtsifz=tnmz=zifz=mts
35 32 34 sylan9eq ¬m=n¬s=tzabwabzawaFz=zifz=mts
36 1 2 unxpdomlem1 wabFw=ifwawifw=mtsifw=tnmw
37 36 ad2antll ¬m=n¬s=tzabwabFw=ifwawifw=mtsifw=tnmw
38 iftrue waifwawifw=mtsifw=tnmw=wifw=mts
39 38 adantl zawaifwawifw=mtsifw=tnmw=wifw=mts
40 37 39 sylan9eq ¬m=n¬s=tzabwabzawaFw=wifw=mts
41 35 40 eqeq12d ¬m=n¬s=tzabwabzawaFz=Fwzifz=mts=wifw=mts
42 vex zV
43 vex tV
44 vex sV
45 43 44 ifex ifz=mtsV
46 42 45 opth1 zifz=mts=wifw=mtsz=w
47 41 46 syl6bi ¬m=n¬s=tzabwabzawaFz=Fwz=w
48 simprr ¬m=n¬s=tzabwabwab
49 simpll ¬m=n¬s=tzabwab¬m=n
50 simplr ¬m=n¬s=tzabwab¬s=t
51 1 2 48 49 50 unxpdomlem2 ¬m=n¬s=tzabwabza¬wa¬Fz=Fw
52 51 pm2.21d ¬m=n¬s=tzabwabza¬waFz=Fwz=w
53 eqcom Fz=FwFw=Fz
54 simprl ¬m=n¬s=tzabwabzab
55 1 2 54 49 50 unxpdomlem2 ¬m=n¬s=tzabwabwa¬za¬Fw=Fz
56 55 ancom2s ¬m=n¬s=tzabwab¬zawa¬Fw=Fz
57 56 pm2.21d ¬m=n¬s=tzabwab¬zawaFw=Fzz=w
58 53 57 biimtrid ¬m=n¬s=tzabwab¬zawaFz=Fwz=w
59 iffalse ¬zaifzazifz=mtsifz=tnmz=ifz=tnmz
60 59 adantr ¬za¬waifzazifz=mtsifz=tnmz=ifz=tnmz
61 32 60 sylan9eq ¬m=n¬s=tzabwab¬za¬waFz=ifz=tnmz
62 iffalse ¬waifwawifw=mtsifw=tnmw=ifw=tnmw
63 62 adantl ¬za¬waifwawifw=mtsifw=tnmw=ifw=tnmw
64 37 63 sylan9eq ¬m=n¬s=tzabwab¬za¬waFw=ifw=tnmw
65 61 64 eqeq12d ¬m=n¬s=tzabwab¬za¬waFz=Fwifz=tnmz=ifw=tnmw
66 vex nV
67 vex mV
68 66 67 ifex ifz=tnmV
69 68 42 opth ifz=tnmz=ifw=tnmwifz=tnm=ifw=tnmz=w
70 69 simprbi ifz=tnmz=ifw=tnmwz=w
71 65 70 syl6bi ¬m=n¬s=tzabwab¬za¬waFz=Fwz=w
72 47 52 58 71 4casesdan ¬m=n¬s=tzabwabFz=Fwz=w
73 72 ralrimivva ¬m=n¬s=tzabwabFz=Fwz=w
74 73 3ad2ant3 masbnatb¬m=n¬s=tzabwabFz=Fwz=w
75 dff13 F:ab1-1a×bF:aba×bzabwabFz=Fwz=w
76 30 74 75 sylanbrc masbnatb¬m=n¬s=tF:ab1-1a×b
77 f1dom2g abVa×bVF:ab1-1a×baba×b
78 11 12 76 77 mp3an12i masbnatb¬m=n¬s=taba×b
79 78 3expia masbnatb¬m=n¬s=taba×b
80 79 rexlimdvva masbnatb¬m=n¬s=taba×b
81 8 80 biimtrrid masbna¬m=ntb¬s=taba×b
82 81 rexlimivv masbna¬m=ntb¬s=taba×b
83 7 82 sylbir mana¬m=nsbtb¬s=taba×b
84 4 6 83 syl2anb 1𝑜a1𝑜baba×b